theorem PiBase.instLindelofSpaceOfHereditarilyLindelofSpace {X : Type u} [TopologicalSpace X] [HereditarilyLindelofSpace X] : LindelofSpace X

Theorem T254: P131 (HereditarilyLindelofSpace) => P18 (LindelofSpace)

theorem PiBase.Formal.T254 : P131 ≤ P18