theorem PiBase.instLocallyCompactSpaceOfWeaklyLocallyCompactSpaceOfRegularSpace {X : Type u} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [RegularSpace X] : LocallyCompactSpace X

Theorem T246: P23 (WeaklyLocallyCompactSpace) + P11 (RegularSpace) => P130 (LocallyCompactSpace)

theorem PiBase.Formal.T246 : P23 ⊓ P11 ≤ P130