instance PiBase.instSoberSpaceOfScatteredSpace {X : Type u} [TopologicalSpace X] [h : ScatteredSpace X] : SoberSpace X

Theorem T865: P51 (ScatteredSpace) => P73 (SoberSpace)

theorem PiBase.Formal.T865 : P51 ≤ P73