theorem PiBase.instCompletelyRegularSpaceOfT35Space {X : Type u} [TopologicalSpace X] [T35Space X] : CompletelyRegularSpace X

Theorem T149: P6 (T35Space) => P12 (CompletelyRegularSpace)

theorem PiBase.Formal.T149 : P6 ≤ P12