Let X and Tx be given.
Assume H: compact_space X Tx.
We prove the intermediate claim Hprop: ∀Fam : set, open_cover_of X Tx Fam → has_finite_subcover X Tx Fam.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀Fam : set, open_cover_of X Tx Fam → has_finite_subcover X Tx Fam) H).
An exact proof term for the current goal is Hprop.
∎