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