proposition: Lemma neighborhood_interior: forall {X:TopologicalSpace} (N:Ensemble X) (x:X), neighborhood N x -> In (interior N) x.
proof: Proof. intros. destruct H as [U]. destruct H. destruct H. assert (Included U (interior N)) by now apply interior_maximal. auto with sets. Qed.
imports: TopologicalSpaces Ensembles InteriorsClosures ZornsLemma(EnsemblesImplicit)