instance PiBase.instPreirreducibleSpaceOfExtremallyDisconnectedOfPreconnectedSpace {X : Type u} [TopologicalSpace X] [h : ExtremallyDisconnected X] [h' : PreconnectedSpace X] : PreirreducibleSpace X

Theorem T97: P49 (ExtremallyDisconnected) + P36 (PreconnectedSpace) => P39 (PreirreducibleSpace)

theorem PiBase.Formal.T97 : P49 ⊓ P36 ≤ P39