theorem PiBase.instT2SpaceOfR1SpaceOfT0Space {X : Type u} [TopologicalSpace X] [R1Space X] [T0Space X] : T2Space X

Theorem T283: P134 (R1Space) + P1 (T0Space) => P3 (T2Space)

theorem PiBase.Formal.T283 : P134 ⊓ P1 ≤ P3