proposition: Lemma family_union_empty_sets (X : Type) (F : Family X) : (forall U, In F U -> U = Empty_set) <-> FamilyUnion F = Empty_set.
proof: Proof. split. - intros. extensionality_ensembles. rewrite <- (H S); auto. - intros. extensionality_ensembles. rewrite <- H. exists U; assumption. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)