theorem PiBase.instExtremallyDisconnectedOfStoneanSpace {X : Type u} [TopologicalSpace X] [StoneanSpace X] : ExtremallyDisconnected X

Theorem T803: P119 (StoneanSpace) => P49 (ExtremallyDisconnected)

theorem PiBase.Formal.T803 : P119 ≤ P49