instance PiBase.instCompletelyRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space {X : Type u} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X] : CompletelyRegularSpace X

Theorem T27: P23 (WeaklyLocallyCompactSpace) + P134 (R1Space) => P12 (CompletelyRegularSpace)

theorem PiBase.Formal.T27 : P23 ⊓ P134 ≤ P12