proposition: Lemma int_family_union: forall (S:Ensemble X) (F:Ensemble (Ensemble X)), In F S -> Included (int S) (int (FamilyUnion F)).
proof: Proof. intros. replace (int S) with (Intersection (int S) (int (FamilyUnion F))). - auto with sets. - rewrite <- int_respects_intersection. f_equal. now apply intersection_family_union. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)