proposition: Lemma neighborhood_upward_closed {X : TopologicalSpace} (x : X) (U V : Ensemble X) : Included U V -> neighborhood U x -> neighborhood V x.
proof: Proof. intros HUV [W []]. exists W; auto. split; auto. transitivity U; auto. Qed.
imports: TopologicalSpaces Ensembles InteriorsClosures ZornsLemma(EnsemblesImplicit)