---

Step * of Lemma eo-strict-forward-locl

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e,a,b:Top].  ((a <loc b) ~ (a <loc b))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``es-le es-locl`` 0
   THEN (RWO "eo-strict-forward-loc" 0 THENA Auto)
   THEN (RWO "eo-strict-forward-less" 0 THENA Auto)
   THEN EqCD) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e,a,b:Top].    ((a  <loc  b)  \msim{}  (a  <loc  b))


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-le  es-locl``  0
  THEN  (RWO  "eo-strict-forward-loc"  0  THENA  Auto)
  THEN  (RWO  "eo-strict-forward-less"  0  THENA  Auto)
  THEN  EqCD)

---

Home Index