theorem PiBase.instR0SpaceOfT1Space {X : Type u} [TopologicalSpace X] [T1Space X] : R0Space X

Theorem T287: P2 (T1Space) => P135 (R0Space)

theorem PiBase.Formal.T287 : P2 ≤ P135