proposition: Lemma B_open_alt (U : Ensemble X) : U = FamilyUnion (fun V : Ensemble X => In B V /\ Included V U) -> B_open U.
proof: Proof. intros. rewrite H. constructor. firstorder. Qed.
imports: Coq(ClassicalChoice) ZornsLemma(CardinalsEns)