theorem PiBase.instNonemptyOfHasGroupTopology {X : Type u} [TopologicalSpace X] [h : HasGroupTopology X] : Nonempty X

Theorem T346: P87 (HasGroupTopology) => P137ᶜ (Nonempty)

theorem PiBase.Formal.T346 : P87 ≤ P137ᶜ