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