instance PiBase.instT0SpaceOfScatteredSpace {X : Type u} [TopologicalSpace X] [h : ScatteredSpace X] : T0Space X

Theorem T169: P51 (ScatteredSpace) => P1 (T0Space)

theorem PiBase.Formal.T169 : P51 ≤ P1