---

Step * of Lemma eo-forward-bless

∀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-locl" (-1)
   THEN AutoBoolCase ⌈a <loc b⌉⋅) }

---

Latex:


\mforall{}eo:EO.  \mforall{}e:E.  \mforall{}a,b:E.    (a  <loc  b  \msim{}  a  <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  <loc  b\mkleeneclose{}\mcdot{}
  THEN  RWO  "eo-forward-locl"  (-1)
  THEN  AutoBoolCase  \mkleeneopen{}a  <loc  b\mkleeneclose{}\mcdot{})

---

Home Index