proposition: Lemma open_finite_intersections (X : TopologicalSpace) : Included (finite_intersections (@open X)) open.
proof: Proof. intros U HU. induction HU; auto. { apply open_full. } apply open_intersection2; assumption. Qed.
imports: ZornsLemma(FiniteIntersections Powerset_facts)