Definition. compl_eq
compl A = {x | ¬x ∈ A}