---

Step * of Lemma es-le-trans

∀the_es:EO. Trans(E;x,y.x ≤loc y )
BY
{ ((Unfolds ``trans es-le`` 0 THEN Auto THEN (InstLemma `es-locl-trans` [⌜the_es⌝])⋅) THENA Auto) }

1
1. the_es : EO@i'
2. a : E@i
3. b : E@i
4. c : E@i
5. (a <loc b) ∨ (a = b ∈ E)@i
6. (b <loc c) ∨ (b = c ∈ E)@i
7. Trans(E;x,y.(x <loc y))
⊢ (a <loc c) ∨ (a = c ∈ E)

---

Latex:

---

Latex:
\mforall{}the$_{es}$:EO.  Trans(E;x,y.x  \mleq{}loc  y  )


By

---

Latex:
((Unfolds  ``trans  es-le``  0  THEN  Auto  THEN  (InstLemma  `es-locl-trans`  [\mkleeneopen{}the$_{es}\mbackslash{}ff\000C24\mkleeneclose{}])\mcdot{})  THENA  Auto)

---

Home Index