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

Theorem T288: P135 (R0Space) + P1 (T0Space) => P2 (T1Space)

theorem PiBase.Formal.T288 : P135 ⊓ P1 ≤ P2