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