theorem PiBase.instNonemptyOfContractibleSpace {X : Type u} [TopologicalSpace X] [h : ContractibleSpace X] : Nonempty X

Theorem T584: P199 (ContractibleSpace) => P137ᶜ (Nonempty)

theorem PiBase.Formal.T584 : P199 ≤ P137ᶜ