theorem PiBase.instNonemptyOfFixedPointSpace {X : Type u} [TopologicalSpace X] [h : FixedPointSpace X] : Nonempty X

Theorem T446: P89 (FixedPointSpace) => P137ᶜ (Nonempty)

theorem PiBase.Formal.T446 : P89 ≤ P137ᶜ