instance PiBase.instLocallyRelativelyCompactSpaceOfWeaklyLocallyCompactSpaceOfKc {X : Type u_1} [TopologicalSpace X] [h : WeaklyLocallyCompactSpace X] [h' : KcSpace X] : LocallyRelativelyCompactSpace X

theorem PiBase.Formal.T81 : P23 ⊓ P100 ≤ P24