proposition: Lemma subfamily_union: forall F G:Family T, Included F G -> Included (FamilyUnion F) (FamilyUnion G).
proof: Proof. unfold Included. intros. destruct H0. apply family_union_intro with S. - apply H. assumption. - assumption. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)