proposition: Lemma open_neighborhood_is_neighborhood: forall {X:TopologicalSpace} (U:Ensemble X) (x:X), open_neighborhood U x -> neighborhood U x.
proof: Proof. intros. exists U. auto with sets. Qed.
imports: TopologicalSpaces Ensembles InteriorsClosures ZornsLemma(EnsemblesImplicit)