proposition: Lemma meets_every_open_neighborhood_impl_closure: forall (S:Ensemble X) (x:X), (forall U:Ensemble X, open U -> In U x -> Inhabited (Intersection S U)) -> In (closure S) x.
proof: Proof. intros. apply NNPP; intro. pose proof (H (Complement (closure S))). destruct H1. - apply closure_closed. - assumption. - destruct H1. contradiction H2. now apply closure_inflationary. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)