---

Step * of Lemma eo-forward-ble

∀eo:EO. ∀e:E. ∀a,b:E.  (a ≤loc b ~ a ≤loc b)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN (Assert eo.e ∈ EO BY
               (BLemma `eo-forward-wf` THEN Auto))
   THEN Auto
   THEN AutoBoolCase ⌈a ≤loc b⌉⋅
   THEN (RWO "eo-forward-le" (-1) THENA Auto)
   THEN AutoBoolCase ⌈a ≤loc b⌉⋅) }

---

Latex:


\mforall{}eo:EO.  \mforall{}e:E.  \mforall{}a,b:E.    (a  \mleq{}loc  b  \msim{}  a  \mleq{}loc  b)


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (Assert  eo.e  \mmember{}  EO  BY
                          (BLemma  `eo-forward-wf`  THEN  Auto))
  THEN  Auto
  THEN  AutoBoolCase  \mkleeneopen{}a  \mleq{}loc  b\mkleeneclose{}\mcdot{}
  THEN  (RWO  "eo-forward-le"  (-1)  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}a  \mleq{}loc  b\mkleeneclose{}\mcdot{})

---

Home Index