proposition: Lemma Build_TopologicalSpace_from_open_neighborhood_bases_basis: forall x:X, open_neighborhood_basis (NB x) x (X:=Build_TopologicalSpace_from_open_neighborhood_bases).
proof: Proof. assert (open_basis (IndexedUnion NB) (X:=Build_TopologicalSpace_from_open_neighborhood_bases)) by apply Build_TopologicalSpace_from_open_basis_basis. destruct H. intros. constructor; intros. - constructor. + apply open_basis_elements. now exists x. + now apply neighborhood_basis_cond2. - destruct H. destruct (open_basis_cover x U H H0) as [V [? []]]. destruct H1 as [y V]. destruct (neighborhood_basis_system_cond y x V H1 H3) as [W []]. exists W. auto with sets. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases