proposition: Lemma Build_TopologicalSpace_from_subbasis_subbasis: @subbasis Build_TopologicalSpace_from_subbasis S.
proof: Proof. assert (@open_basis Build_TopologicalSpace_from_subbasis (finite_intersections S)). { apply Build_TopologicalSpace_from_open_basis_basis. } constructor. - intros. simpl in U. apply open_basis_elements with (finite_intersections S); trivial. constructor; trivial. - intros. destruct (@open_basis_cover _ _ H x U) as [V]; trivial. destruct H2 as [? [? ?]]. simpl. exists V. repeat split; auto. Qed.
imports: ZornsLemma(FiniteIntersections) ZornsLemma(FiniteIntersections)