---

Step * 1 1 1 of Lemma ex-approx_transitivity


1. e : Atom2
2. t1 : Base
3. t2 : Base
4. t3 : Base
5. ∀f:Base. (e#f:Base ⇒ (f t1?e:v.⊥ ≤ f t2?e:v.⊥))
6. f : Base
7. e#f:Base
8. f t2?e:v.⊥ ≤ f t3?e:v.⊥
9. f t1?e:v.⊥ ≤ f t2?e:v.⊥
⊢ f t1?e:v.⊥ ≤ f t3?e:v.⊥
BY
{ (FLemma `sqle_trans` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  Atom2
2.  t1  :  Base
3.  t2  :  Base
4.  t3  :  Base
5.  \mforall{}f:Base.  (e\#f:Base  {}\mRightarrow{}  (f  t1?e:v.\mbot{}  \mleq{}  f  t2?e:v.\mbot{}))
6.  f  :  Base
7.  e\#f:Base
8.  f  t2?e:v.\mbot{}  \mleq{}  f  t3?e:v.\mbot{}
9.  f  t1?e:v.\mbot{}  \mleq{}  f  t2?e:v.\mbot{}
\mvdash{}  f  t1?e:v.\mbot{}  \mleq{}  f  t3?e:v.\mbot{}


By

---

Latex:
(FLemma  `sqle\_trans`  [-1;-2]  THEN  Auto)

---

Home Index