instance PiBase.instGoSpaceOfLots {X : Type u} [τ : TopologicalSpace X] [h : Lots X] : GoSpace X

Theorem T66: P133 (Lots) => P154 (GoSpace)

theorem PiBase.Formal.T66 : P133 ≤ P154