Definition. DiagCl_eq
DiagCl = {x | ¬x ∈ x}