class PiBase.DoorSpace (X : Type u) [TopologicalSpace X] : Prop

• isOpen_or_isClosed (s : Set X) : IsOpen s ∨ IsClosed s