proposition: Lemma family_intersection_add {X : Type} (F : Family X) (U : Ensemble X) : FamilyIntersection (Add F U) = Intersection (FamilyIntersection F) U.
proof: Proof. apply Extensionality_Ensembles; split; red; intros; constructor. - constructor. destruct H. intros. apply H. left. assumption. - destruct H. apply H. right. reflexivity. - intros. destruct H. destruct H. destruct H0. + apply H. assumption. + inversion H0; subst; clear H0. assumption. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)