---

Step * of Lemma implies-es-le-pred

∀the_es:EO. ∀e,e':E.  ((e <loc e') ⇒ e ≤loc pred(e') )
BY
{ (Auto THEN RWO "es-le-pred" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}the$_{es}$:EO.  \mforall{}e,e':E.    ((e  <loc  e')  {}\mRightarrow{}  e  \mleq{}loc  pred(e')  )


By

---

Latex:
(Auto  THEN  RWO  "es-le-pred"  0  THEN  Auto)

---

Home Index