instance PiBase.instFiniteOfAnticompactSpaceOfCompactSpace {X : Type u} [TopologicalSpace X] [h : AnticompactSpace X] [h' : CompactSpace X] : Finite X

Theorem T303: P136 (AnticompactSpace) + P16 (CompactSpace) => P78 (Finite)

theorem PiBase.Formal.T303 : P136 ⊓ P16 ≤ P78