theorem PiBase.instCompactSpaceOfContinuumSpace {X : Type u} [TopologicalSpace X] [ContinuumSpace X] : CompactSpace X

Theorem T482: P188 (ContinuumSpace) => P16 (CompactSpace)

theorem PiBase.Formal.T482 : P188 ≤ P16