proposition: Lemma finite_intersections_of_subbasis_form_open_basis: subbasis -> open_basis (finite_intersections SB).
proof: Proof. constructor. - intros. induction H0; auto with topology. apply H. assumption. - intros. pose proof (subbasis_cover H U x H1 H0) as [V [? []]]. exists V. repeat split; auto. Qed.
imports: ZornsLemma(FiniteIntersections)