proposition: Lemma Complement_Empty_set {X : Type} : Complement (@Empty_set X) = Full_set.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - constructor. - intro. destruct H0. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)