fact: Definition neighborhood {X:TopologicalSpace} (N:Ensemble X) (x:X) := exists U:Ensemble X, open_neighborhood U x /\ Included U N.
imports: TopologicalSpaces Ensembles InteriorsClosures ZornsLemma(EnsemblesImplicit)