theorem PiBase.instNonemptyOfHasDispersionPoint {X : Type u} [TopologicalSpace X] [HasDispersionPoint X] : Nonempty X

Theorem T41: P45 (HasDispersionPoint) => P137 (¬IsEmpty)

theorem PiBase.Formal.T41 : P45 ≤ P137ᶜ