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