theorem PiBase.instT35SpaceOfCompletelyRegularSpaceOfT0Space {X : Type u} [TopologicalSpace X] [h : CompletelyRegularSpace X] [h' : T0Space X] : T35Space X

Theorem T151: P12 (CompletelyRegularSpace) + P1 (T0Space) => P6 (T35Space)

theorem PiBase.Formal.T151 : P12 ⊓ P1 ≤ P6