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

Theorem T245: P130 (LocallyCompactSpace) => P23 (WeaklyLocallyCompactSpace)

theorem PiBase.Formal.T245 : P130 ≤ P23