---

Step * of Lemma es-causle-trans

∀the_es:EO. Trans(E;x,y.x c≤ y)
BY
{ ((Unfolds ``trans es-causle`` 0 THEN Auto THEN (InstESAxiom ⌜the_es⌝ [] 6)⋅) THENA Auto) }

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

---

Latex:

---

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


By

---

Latex:
((Unfolds  ``trans  es-causle``  0  THEN  Auto  THEN  (InstESAxiom  \mkleeneopen{}the$_{es}$\mkleeneclose{}  []  6)\mcdot{})\000C  THENA  Auto)

---

Home Index