Let X, Tx, seq and x be given.
Assume H: converges_to X Tx seq x.
We prove the intermediate claim H123: (topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X.
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ sequence_on seq X) ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U) H).
We prove the intermediate claim H12: topology_on X Tx ∧ sequence_on seq X.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ sequence_on seq X) (x ∈ X) H123).
An exact proof term for the current goal is (andER (topology_on X Tx) (sequence_on seq X) H12).
∎