instance PiBase.instScatteredSpaceOfAlmostDiscreteSpace {X : Type u} [TopologicalSpace X] [h : AlmostDiscreteSpace X] : ScatteredSpace X

Theorem T573: P203 (AlmostDiscreteSpace) => P51 (ScatteredSpace)

theorem PiBase.Formal.T573 : P203 ≤ P51