proposition: Lemma open_neighborhood_basis_is_neighborhood_basis: forall {X:TopologicalSpace} (NB:Family X) (x:point_set X), open_neighborhood_basis NB x -> neighborhood_basis NB x.
proof: Proof. intros. destruct H. constructor; intros. - apply open_neighborhood_is_neighborhood. auto. - destruct H as [U [? ?]]. destruct (open_neighborhood_basis_cond0 U H) as [V [? ?]]. exists V. split; auto with sets. Qed.
imports: TopologicalSpaces Neighborhoods OpenBases