proposition: Lemma closure_impl_meets_every_open_neighborhood: forall (S:Ensemble X) (x:X), In (closure S) x -> forall U:Ensemble X, open U -> In U x -> Inhabited (Intersection S U).
proof: Proof. intros. apply NNPP; intro. assert (Included (closure S) (Complement U)). { apply closure_minimal. - unfold closed. now rewrite Complement_Complement. - red; intros. intro. contradiction H2. exists x0; constructor; trivial. } contradict H1. now apply H3. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)