Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ 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 HexN to the current goal.

Let N be given.

Assume HNpair: N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun seq n ∈ U.

We prove the intermediate claim HNO: N ∈ ω.

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

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

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

We prove the intermediate claim HNinU: apply_fun seq N ∈ U.

An exact proof term for the current goal is (Htail N HNO (Subq_ref N)).

We prove the intermediate claim HNinA: apply_fun seq N ∈ A.

An exact proof term for the current goal is (HseqA N HNO).

We prove the intermediate claim HNinUA: apply_fun seq N ∈ U ∩ A.

An exact proof term for the current goal is (binintersectI U A (apply_fun seq N) HNinU HNinA).

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