theorem PiBase.instLocallyCompactSpaceOfSpectralSpace {X : Type u} [TopologicalSpace X] [SpectralSpace X] : LocallyCompactSpace X

Theorem T527: P75 (SpectralSpace) => P130 (LocallyCompactSpace)

theorem PiBase.Formal.T527 : P75 ≤ P130