proposition: Lemma dense_meets_every_nonempty_open: forall S:Ensemble X, dense S -> forall U:Ensemble X, open U -> Inhabited U -> Inhabited (Intersection S U).
proof: Proof. intros. destruct H1. apply closure_impl_meets_every_open_neighborhood with x; trivial. rewrite H; constructor. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)