theorem PiBase.instSoberSpaceOfSpectralSpace {X : Type u} [TopologicalSpace X] [SpectralSpace X] : SoberSpace X

Theorem T176: P75 (SpectralSpace) => P73 (SoberSpace)

theorem PiBase.Formal.T176 : P75 ≤ P73