Let X, Tx, Y, d, fn, eps and x be given.

Assume HTx: topology_on X Tx.

Assume Hx: x ∈ U_eps X Tx Y d fn eps.

Set UFam to be the term {interior_of X Tx (A_N_eps X Y d fn N eps)|N ∈ ω}.

We prove the intermediate claim HUdef: U_eps X Tx Y d fn eps = ⋃ UFam.

Use reflexivity.

We prove the intermediate claim HxUnion: x ∈ ⋃ UFam.

rewrite the current goal using HUdef (from right to left).

An exact proof term for the current goal is Hx.

Apply (UnionE_impred UFam x HxUnion (∃N : set, N ∈ ω ∧ ∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ⊆ A_N_eps X Y d fn N eps)) to the current goal.

Let W be given.

Assume HxW: x ∈ W.

Assume HWUFam: W ∈ UFam.

Apply (ReplE_impred ω (λN0 : set ⇒ interior_of X Tx (A_N_eps X Y d fn N0 eps)) W HWUFam (∃N : set, N ∈ ω ∧ ∃U : set, U ∈ Tx ∧ x ∈ U ∧ U ⊆ A_N_eps X Y d fn N eps)) to the current goal.

Let N be given.

Assume HN: N ∈ ω.

Assume HWdef: W = interior_of X Tx (A_N_eps X Y d fn N eps).

We prove the intermediate claim HxInt: x ∈ interior_of X Tx (A_N_eps X Y d fn N eps).

rewrite the current goal using HWdef (from right to left).

An exact proof term for the current goal is HxW.

We prove the intermediate claim HintDef: interior_of X Tx (A_N_eps X Y d fn N eps) = {x0 ∈ X|∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N eps)}.

Use reflexivity.

We prove the intermediate claim HexU0: ∃U0 : set, U0 ∈ Tx ∧ x ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N eps).

We prove the intermediate claim HxInt2: x ∈ {x0 ∈ X|∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N eps)}.

rewrite the current goal using HintDef (from right to left).

An exact proof term for the current goal is HxInt.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃U0 : set, U0 ∈ Tx ∧ x0 ∈ U0 ∧ U0 ⊆ (A_N_eps X Y d fn N eps)) x HxInt2).

Apply HexU0 to the current goal.

Let U be given.

Assume HU: U ∈ Tx ∧ x ∈ U ∧ U ⊆ (A_N_eps X Y d fn N eps).

We use N to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HN.

We use U to witness the existential quantifier.

An exact proof term for the current goal is HU.

∎