instance PiBase.instWeaklyLocallyCompactSpaceOfExhaustibleByCompacts {X : Type u} [TopologicalSpace X] [h : ExhaustibleByCompacts X] : WeaklyLocallyCompactSpace X

Theorem T8: P25 (ExhaustibleByCompacts) => P23 (WeaklyLocallyCompactSpace)

theorem PiBase.Formal.T8 : P25 ≤ P23