Let X, Y, d, fn, N, eps1 and eps2 be given.
Assume Heps1R: eps1 ∈ R.
Assume Heps2R: eps2 ∈ R.
Assume Heps12: Rle eps1 eps2.
We will prove A_N_eps X Y d fn N eps1 ⊆ A_N_eps X Y d fn N eps2.
Let x be given.
Assume Hx: x ∈ A_N_eps X Y d fn N eps1.
We will prove x ∈ A_N_eps X Y d fn N eps2.
We prove the intermediate claim HdefA2: A_N_eps X Y d fn N eps2 = {x0 ∈ X|∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps2}.
Use reflexivity.
rewrite the current goal using HdefA2 (from left to right).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps1) x Hx).
We prove the intermediate claim HxProp: ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps1) x Hx).
Apply (SepI X (λx0 : set ⇒ ∀n : set, n ∈ ω → N ⊆ n → ∀m : set, m ∈ ω → N ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps2) x HxX) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N ⊆ n.
Let m be given.
Assume HmO: m ∈ ω.
Assume HNm: N ⊆ m.
We prove the intermediate claim Hle1: Rle (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps1.
An exact proof term for the current goal is (HxProp n HnO HNn m HmO HNm).
An exact proof term for the current goal is (Rle_tra (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps1 eps2 Hle1 Heps12).
∎