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

Theorem T281: P3 (T2Space) => P134 (R1Space)

theorem PiBase.Formal.T281 : P3 ≤ P134