---

Step * of Lemma ex-approx_transitivity

∀[e:Atom2]. ∀[t1,t2,t3:Base].  (ex-approx(e;t1;t3)) supposing (ex-approx(e;t1;t2) and ex-approx(e;t2;t3))
BY
{ ((Intros THEN (Unhide THENA Auto)) THEN All (Unfold `ex-approx`)) }

1
1. e : Atom2
2. t1 : Base
3. t2 : Base
4. t3 : Base
5. ∀f:Base. (e#f:Base ⇒ (f t2?e:v.⊥ ≤ f t3?e:v.⊥))
6. ∀f:Base. (e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t2?e:v.⊥))
⊢ ∀f:Base. (e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t3?e:v.⊥))

---

Latex:

---

Latex:
\mforall{}[e:Atom2].  \mforall{}[t1,t2,t3:Base].
    (ex-approx(e;t1;t3))  supposing  (ex-approx(e;t1;t2)  and  ex-approx(e;t2;t3))


By

---

Latex:
((Intros  THEN  (Unhide  THENA  Auto))  THEN  All  (Unfold  `ex-approx`))

---

Home Index