theorem PiBase.instR1SpaceOfRegularSpace {X : Type u} [TopologicalSpace X] [RegularSpace X] : R1Space X

Theorem T282: P11 (RegularSpace) => P134 (R1Space)

theorem PiBase.Formal.T282 : P11 ≤ P134