theorem PiBase.not_DiscreteTopologyOfAlmostDiscreteSpace {X : Type u} [TopologicalSpace X] [h : AlmostDiscreteSpace X] : ¬DiscreteTopology X

Theorem T571: P203 (AlmostDiscreteSpace) => P52 (¬DiscreteTopology)

theorem PiBase.Formal.T571 : P203 ≤ P52ᶜ