proposition: Lemma FamilyIntersection_In_Included {X : Type} (F : Family X) (U : Ensemble X) : In F U -> Included (FamilyIntersection F) U.
proof: Proof. intros HU x Hx. destruct Hx. apply H, HU. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)