theorem PiBase.instStoneSpaceOfCompactSpaceOfT2SpaceOfTotallyDisconnectedSpace {X : Type u} [TopologicalSpace X] [h : CompactSpace X] [h' : T2Space X] [h'' : TotallyDisconnectedSpace X] : StoneSpace X

Theorem T529: P16 (CompactSpace) + P3 (T2Space) + P47 (TotallyDisconnectedSpace) => P195 (StoneSpace)

theorem PiBase.Formal.T529 : P16 ⊓ P3 ⊓ P47 ≤ P195