theorem PiBase.instT3SpaceOfRegularSpaceOfT0Space {X : Type u} [TopologicalSpace X] [RegularSpace X] [T0Space X] : T3Space X

Theorem T148: P11 (RegularSpace) + P1 (T0Space) => P5 (T3Space)

theorem PiBase.Formal.T148 : P11 ⊓ P1 ≤ P5