Let X, Tx and A be given.

Assume HH: Hausdorff_space X Tx.

Assume HA: A ⊆ X.

Assume Hcomp: compact_space A (subspace_topology X Tx A).

We will prove closed_in X Tx A.

An exact proof term for the current goal is (compact_subspace_in_Hausdorff_closed X Tx A HH HA Hcomp).

∎