proposition: Lemma Lindelof_degree_exists (X : TopologicalSpace) : exists (Y : Type) (kappa : Ensemble Y), Lindelof_degree X kappa.
proof: Proof. unfold Lindelof_degree. apply least_cardinal_exists with (X := Ensemble X) (U := @open X). apply Lindelof_Lemma_technical'. firstorder. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)