Let X, Tx, A, seq and x be given.
Assume HTx: topology_on X Tx.
Assume HAsub: A ⊆ X.
Assume HAclosed: closed_in X Tx A.
Assume Hxlim: converges_to X Tx seq x.
Assume HseqA: ∀n : set, n ∈ ω → apply_fun seq n ∈ A.
We will prove x ∈ A.
We prove the intermediate claim Hxcl: x ∈ closure_of X Tx A.
An exact proof term for the current goal is (converges_to_imp_in_closure_of_terms X Tx A seq x Hxlim HseqA).
We prove the intermediate claim HclEq: closure_of X Tx A = A.
An exact proof term for the current goal is (closed_closure_eq X Tx A HTx HAclosed).
rewrite the current goal using HclEq (from right to left).
An exact proof term for the current goal is Hxcl.
∎