proposition: Lemma Build_TopologicalSpace_from_open_basis_basis: @open_basis Build_TopologicalSpace_from_open_basis B.
proof: Proof. constructor. - intros. simpl. rewrite <- family_union_singleton. constructor. red. intros. now destruct H0. - simpl. intros. destruct H, H0. exists S. repeat split; auto with sets. red. intros. now exists S. Qed.
imports: Coq(ClassicalChoice) ZornsLemma(CardinalsEns)