instance PiBase.instWeaklyLindelofSpaceOfLindelofSpace {X : Type u} [TopologicalSpace X] [h : LindelofSpace X] : WeaklyLindelofSpace X

Theorem T128: P18 (LindelofSpace) => P62 (WeaklyLindelofSpace)

theorem PiBase.Formal.T128 : P18 ≤ P62