proposition: Lemma Union_Complement_r {X} (U : Ensemble X) : Union U (Complement U) = Full_set.
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - constructor. - destruct (classic (In U x)); [left|right]; assumption. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)