theorem PiBase.instSeparableSpaceOfPolishSpace {X : Type u} [TopologicalSpace X] [PolishSpace X] : TopologicalSpace.SeparableSpace X

Theorem T199: P116 (PolishSpace) => P26 (SeparableSpace)

theorem PiBase.Formal.T199 : P116 ≤ P26