theorem PiBase.instArtinianSpaceOfFinite {X : Type u} [TopologicalSpace X] [Finite X] : ArtinianSpace X

Theorem T825: P78 (Finite) => P226 (ArtinianSpace)

theorem PiBase.Formal.T825 : P78 ≤ P226