Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We prove the intermediate claim HexN1: ∃N1 : set, N1 ∈ ω ∧ ∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seq n ∈ U.

An exact proof term for the current goal is (converges_to_neighborhoods X Tx seq x Hxlim U HU HxU).

Apply HexN1 to the current goal.

Let N1 be given.

Assume HN1pair: N1 ∈ ω ∧ ∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seq n ∈ U.

We prove the intermediate claim HN1omega: N1 ∈ ω.

An exact proof term for the current goal is (andEL (N1 ∈ ω) (∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seq n ∈ U) HN1pair).

We prove the intermediate claim HtailU: ∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seq n ∈ U.

An exact proof term for the current goal is (andER (N1 ∈ ω) (∀n : set, n ∈ ω → N1 ⊆ n → apply_fun seq n ∈ U) HN1pair).

Set n0 to be the term N ∪ N1.

We prove the intermediate claim Hn0omega: n0 ∈ ω.

An exact proof term for the current goal is (omega_binunion N N1 HNomega HN1omega).

We prove the intermediate claim HNsubn0: N ⊆ n0.

An exact proof term for the current goal is (binunion_Subq_1 N N1).

We prove the intermediate claim HN1subn0: N1 ⊆ n0.

An exact proof term for the current goal is (binunion_Subq_2 N N1).

We prove the intermediate claim Hn0inU: apply_fun seq n0 ∈ U.

An exact proof term for the current goal is (HtailU n0 Hn0omega HN1subn0).

We prove the intermediate claim Hn0inA: apply_fun seq n0 ∈ A.

An exact proof term for the current goal is (HtailA n0 Hn0omega HNsubn0).

We prove the intermediate claim Hn0inUA: apply_fun seq n0 ∈ U ∩ A.

An exact proof term for the current goal is (binintersectI U A (apply_fun seq n0) Hn0inU Hn0inA).

An exact proof term for the current goal is (elem_implies_nonempty (U ∩ A) (apply_fun seq n0) Hn0inUA).