Let X, Tx, Y, d, fn, eps1 and eps2 be given.
Assume HTx: topology_on X Tx.
Assume Heps1R: eps1 ∈ R.
Assume Heps2R: eps2 ∈ R.
Assume Heps12: Rle eps1 eps2.
We will prove U_eps X Tx Y d fn eps1 ⊆ U_eps X Tx Y d fn eps2.
Let x be given.
Assume Hx: x ∈ U_eps X Tx Y d fn eps1.
We will prove x ∈ U_eps X Tx Y d fn eps2.
Set Fam1 to be the term {interior_of X Tx (A_N_eps X Y d fn N eps1)|N ∈ ω}.
Set Fam2 to be the term {interior_of X Tx (A_N_eps X Y d fn N eps2)|N ∈ ω}.
We prove the intermediate claim HU1: U_eps X Tx Y d fn eps1 = ⋃ Fam1.
Use reflexivity.
We prove the intermediate claim HU2: U_eps X Tx Y d fn eps2 = ⋃ Fam2.
Use reflexivity.
We prove the intermediate claim HxU1: x ∈ ⋃ Fam1.
rewrite the current goal using HU1 (from right to left).
An exact proof term for the current goal is Hx.
rewrite the current goal using HU2 (from left to right).
Apply (UnionE_impred Fam1 x HxU1 (x ∈ ⋃ Fam2)) to the current goal.
Let W be given.
Assume HxW: x ∈ W.
Assume HW1: W ∈ Fam1.
Apply (ReplE_impred ω (λN0 : set ⇒ interior_of X Tx (A_N_eps X Y d fn N0 eps1)) W HW1 (x ∈ ⋃ Fam2)) 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 eps1).
We prove the intermediate claim HxInt1: x ∈ interior_of X Tx (A_N_eps X Y d fn N eps1).
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 HAmon: A_N_eps X Y d fn N eps1 ⊆ A_N_eps X Y d fn N eps2.
An exact proof term for the current goal is (A_N_eps_monotone X Y d fn N eps1 eps2 Heps1R Heps2R Heps12).
We prove the intermediate claim HintMon: interior_of X Tx (A_N_eps X Y d fn N eps1) ⊆ interior_of X Tx (A_N_eps X Y d fn N eps2).
An exact proof term for the current goal is (interior_monotone X Tx (A_N_eps X Y d fn N eps1) (A_N_eps X Y d fn N eps2) HTx HAmon).
We prove the intermediate claim HxInt2: x ∈ interior_of X Tx (A_N_eps X Y d fn N eps2).
An exact proof term for the current goal is (HintMon x HxInt1).
We prove the intermediate claim HWin2: interior_of X Tx (A_N_eps X Y d fn N eps2) ∈ Fam2.
An exact proof term for the current goal is (ReplI ω (λN0 : set ⇒ interior_of X Tx (A_N_eps X Y d fn N0 eps2)) N HN).
An exact proof term for the current goal is (UnionI Fam2 x (interior_of X Tx (A_N_eps X Y d fn N eps2)) HxInt2 HWin2).
∎