Let X, Tx and Fam be given.

Assume Hcomp: compact_space X Tx.

Assume HFam: open_cover_of X Tx Fam.

We will prove has_finite_subcover X Tx Fam.

An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp Fam HFam).

∎