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

Theorem T146: P5 (T3Space) => P11 (RegularSpace)

theorem PiBase.Formal.T146 : P5 ≤ P11