proposition: Lemma open_finite_family_intersection: forall {X:TopologicalSpace} (F:Family X), Finite F -> (forall U, In F U -> open U) -> open (FamilyIntersection F).
proof: Proof. intros. induction H. - rewrite empty_family_intersection. apply open_full. - rewrite family_intersection_add. apply open_intersection2. + apply IHFinite. intros. apply H0. left. assumption. + apply H0. right. reflexivity. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)