proposition: Lemma weight_unique (X : TopologicalSpace) : forall {Y0 Y1 : Type} (kappa : Ensemble Y0) (lambda : Ensemble Y1), weight X kappa -> weight X lambda -> eq_cardinal_ens kappa lambda.
proof: Proof. intros. eapply least_cardinal_unique; eauto. Qed.
imports: Coq(ClassicalChoice) ZornsLemma(CardinalsEns)