theorem PiBase.instCompactSpaceOfSpectralSpace {X : Type u} [TopologicalSpace X] [SpectralSpace X] : CompactSpace X

Theorem T339: P75 (SpectralSpace) => P16 (CompactSpace)

theorem PiBase.Formal.T339 : P75 ≤ P16