theorem PiBase.instR0SpaceOfR1Space {X : Type u} [TopologicalSpace X] [R1Space X] : R0Space X

Theorem T286: P134 (R1Space) => P135 (R0Space)

theorem PiBase.Formal.T286 : P134 ≤ P135