instance PiBase.instHasGenericPointOfQuasiSoberOfPreirreducibleSpaceOfNonempty {X : Type u} [TopologicalSpace X] [h : QuasiSober X] [h' : PreirreducibleSpace X] [h'' : Nonempty X] : HasGenericPoint X

Theorem T594: P192 (QuasiSober) + P39 (PreirreducibleSpace) + P137 (¬IsEmpty) => P201 (HasGenericPoint)

theorem PiBase.Formal.T594 : P192 ⊓ P39 ⊓ P137ᶜ ≤ P201