proposition: Corollary Lindelof_Lemma_technical' (X : TopologicalSpace) (B : Family X) : open_basis B -> Lindelof_degree_candidate X B.
proof: Proof. intros HB. intros C HC. apply Lindelof_Lemma_technical; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(Classical_Wf DecidableDec FiniteIntersections InfiniteTypes) Coq(RelationClasses)