proposition: Lemma empty_family_union: FamilyUnion (@Empty_set (Ensemble T)) = Empty_set.
proof: Proof. apply Extensionality_Ensembles. unfold Same_set. unfold Included. intuition. - destruct H. contradiction H. - contradiction H. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)