proposition: Lemma meets_every_nonempty_open_impl_dense: forall S:Ensemble X, (forall U:Ensemble X, open U -> Inhabited U -> Inhabited (Intersection S U)) -> dense S.
proof: Proof. intros. extensionality_ensembles. - constructor. - apply meets_every_open_neighborhood_impl_closure. intros. apply H; trivial. now exists x. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)