instance PiBase.instT0SpaceOfDoorSpace {X : Type u} [TopologicalSpace X] [h : DoorSpace X] : T0Space X

Theorem T143: P126 (DoorSpace) => P1 (T0Space)

theorem PiBase.Formal.T143 : P126 ≤ P1