instance PiBase.instLindelofSpaceOfOmegaLindelof {X : Type u} [TopologicalSpace X] [h : OmegaLindelof X] : LindelofSpace X

Theorem T360: P149 (OmegaLindelof) => P18 (LindelofSpace)

theorem PiBase.Formal.T360 : P149 ≤ P18