theorem PiBase.instNoetherianSpaceOfFinite {X : Type u} [TopologicalSpace X] [Finite X] : TopologicalSpace.NoetherianSpace X

Theorem T198: P78 (Finite) => P208 (NoetherianSpace)

theorem PiBase.Formal.T198 : P78 ≤ P208