instance PiBase.instExhaustibleByCompactsOfCompactSpace {X : Type u} [TopologicalSpace X] [CompactSpace X] : ExhaustibleByCompacts X

Theorem T9: P16 (CompactSpace) => P25 (ExhaustibleByCompacts)

theorem PiBase.Formal.T9 : P16 ≤ P25