theorem PiBase.instCompactSpaceOfCorsonCompactSpace {X : Type u} [TopologicalSpace X] [CorsonCompactSpace X] : CompactSpace X

Theorem T457: P77 (CorsonCompactSpace) => P16 (CompactSpace)

theorem PiBase.Formal.T457 : P77 ≤ P16