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

• ex_nbhd_lots (x : X) : ∃ s ∈ nhds x, Lots ↑s