theorem PiBase.instTorontoSpaceOfDiscreteTopology {X : Type u} [TopologicalSpace X] [DiscreteTopology X] : TorontoSpace X

Theorem T817: P52 (DiscreteTopology) => P219 (TorontoSpace)

theorem PiBase.Formal.T817 : P52 ≤ P219