theorem PiBase.instContinuumSpaceOfCompactSpaceOfPreconnectedSpaceOfT2Space {X : Type u} [TopologicalSpace X] [CompactSpace X] [PreconnectedSpace X] [T2Space X] : ContinuumSpace X

Theorem T480: P16 (CompactSpace) + P36 (PreconnectedSpace) + P3 (T2Space) => P188 (ContinuumSpace)

theorem PiBase.Formal.T480 : P16 ⊓ P36 ⊓ P3 ≤ P188