Let X, Tx and F be given.

Assume H: T1_space X Tx.

Assume HFsub: F ⊆ X.

Assume HFfin: finite F.

We prove the intermediate claim Hfin: ∀G : set, G ⊆ X → finite G → closed_in X Tx G.

An exact proof term for the current goal is (andER (topology_on X Tx) (∀G : set, G ⊆ X → finite G → closed_in X Tx G) H).

An exact proof term for the current goal is (Hfin F HFsub HFfin).

∎