instance PiBase.instWeaklyLocallyCompactSpaceOfLocallyRelativelyCompactSpace {X : Type u} [TopologicalSpace X] [h : LocallyRelativelyCompactSpace X] : WeaklyLocallyCompactSpace X

Theorem T7: P24 (LocallyRelativelyCompactSpace) => P23 (WeaklyLocallyCompactSpace)

theorem PiBase.Formal.T7 : P24 ≤ P23