---

Step * of Lemma es-interval-ordered

∀es:EO. ∀e1,e2:E.  l-ordered(E;e1,e2.(e1 <loc e2);[e1, e2])
BY
{ (Auto THEN (D 0 THEN Auto) THEN RWO "l_before-es-interval" (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e1,e2:E.    l-ordered(E;e1,e2.(e1  <loc  e2);[e1,  e2])


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  RWO  "l\_before-es-interval"  (-1)  THEN  Auto)

---

Home Index