proposition: Lemma weight_exists (X : TopologicalSpace) : exists (kappa : Family X), weight X kappa.
proof: Proof. apply least_cardinal_ext_exists. exists open. firstorder. Qed.
imports: Coq(ClassicalChoice) ZornsLemma(CardinalsEns)