instance PiBase.instHereditarilyLindelofSpaceOfNoetherianSpace {X : Type u} [TopologicalSpace X] [h : TopologicalSpace.NoetherianSpace X] : HereditarilyLindelofSpace X

Theorem T657: P208 (NoetherianSpace) => P131 (HereditarilyLindelofSpace)

theorem PiBase.Formal.T657 : P208 ≤ P131