An exact proof term for the current goal is (andER ((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).