instance PiBase.instPSpaceOfAlexandrovDiscrete {X : Type u} [TopologicalSpace X] [AlexandrovDiscrete X] : PSpace X

Theorem T350: P90 (AlexandrovDiscrete) => P147 (PSpace)

theorem PiBase.Formal.T350 : P90 ≤ P147