instance PiBase.instDoorSpaceOfDiscreteTopology {X : Type u} [TopologicalSpace X] [h : DiscreteTopology X] : DoorSpace X

Theorem T144: P52 (DiscreteTopology) => P126 (DoorSpace)

theorem PiBase.Formal.T144 : P52 ≤ P126