proposition: Lemma interior_neighborhood: forall {X:TopologicalSpace} (N:Ensemble X) (x:X), In (interior N) x -> neighborhood N x.
proof: Proof. intros. exists (interior N). repeat split; trivial. - apply interior_open. - apply interior_deflationary. Qed.
imports: TopologicalSpaces Ensembles InteriorsClosures ZornsLemma(EnsemblesImplicit)