proposition: Lemma coverable_by_open_basis_impl_open: forall U:Ensemble X, (forall x:X, In U x -> exists V:Ensemble X, In B V /\ Included V U /\ In V x) -> open U.
proof: Proof. intros. replace U with (FamilyUnion [ V:Ensemble X | In B V /\ Included V U ]). - apply open_family_union. intros. destruct H0. destruct H0. now apply open_basis_elements. - extensionality_ensembles. + destruct H0. auto with sets. + destruct (H x H0) as [V]. destruct H1 as [? [? ?]]. exists V; auto. constructor; auto. Qed.
imports: Coq(ClassicalChoice) ZornsLemma(CardinalsEns)