---

Step * of Lemma es-locl-test2

∀es:EO. ∀e1,e2,e3:E.  ((e1 <loc e2) ⇒ (e2 <loc e3) ⇒ (e1 <loc e3))
BY
{ (UnivCD THENA Auto) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. e3 : E@i
5. (e1 <loc e2)@i
6. (e2 <loc e3)@i
⊢ (e1 <loc e3)

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2,e3:E.    ((e1  <loc  e2)  {}\mRightarrow{}  (e2  <loc  e3)  {}\mRightarrow{}  (e1  <loc  e3))


By

(UnivCD  THENA  Auto)

---

Home Index