instance PiBase.instDoorSpaceOfAlmostDiscreteSpace {X : Type u} [TopologicalSpace X] [h : AlmostDiscreteSpace X] : DoorSpace X

Theorem T572: P203 (AlmostDiscreteSpace) => P126 (DoorSpace)

theorem PiBase.Formal.T572 : P203 ≤ P126