theorem PiBase.instStoneanSpaceOfCompactSpaceOfT2SpaceOfExtremallyDisconnected {X : Type u} [TopologicalSpace X] [CompactSpace X] [T2Space X] [ExtremallyDisconnected X] : StoneanSpace X

Theorem T126: P16 (CompactSpace) + P3 (T2Space) + P49 (ExtremallyDisconnected) => P119 (StoneanSpace)

theorem PiBase.Formal.T126 : P16 ⊓ P3 ⊓ P49 ≤ P119