instance PiBase.instLocallyOrderableSpaceOfLots {X : Type u} [TopologicalSpace X] [h : Lots X] : LocallyOrderableSpace X

Theorem T750: P133 (Lots) => P120 (LocallyOrderableSpace)

theorem PiBase.Formal.T750 : P133 ≤ P120