instance PiBase.instExtremallyDisconnectedOfPreirreducibleSpace {X : Type u} [TopologicalSpace X] [h : PreirreducibleSpace X] : ExtremallyDisconnected X

Theorem T96: P39 (PreirreducibleSpace) => P49 (ExtremallyDisconnected)

theorem PiBase.Formal.T96 : P39 ≤ P49