theorem PiBase.instCompactSpaceOfLindelofSpaceOfCountablyCompactSpace {X : Type u} [TopologicalSpace X] [LindelofSpace X] [h : CountablyCompactSpace X] : CompactSpace X

Theorem T106: P18 (LindelofSpace) + P19 (CountablyCompactSpace) => P16 (CompactSpace)

theorem PiBase.Formal.T106 : P18 ⊓ P19 ≤ P16