---

Step * of Lemma es-interval-sorted-by

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

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2:E.    sorted-by(\mlambda{}e1,e2.  (e1  <loc  e2);[e1,  e2])


By

(Auto
  THEN  (BLemma  `l-ordered-is-sorted-by`  THENA  Auto)
  THEN  (D  0  THEN  Auto)
  THEN  RWO  "l\_before-es-interval"  (-1)
  THEN  Auto)

---

Home Index