---

Step * of Lemma eo-forward-locl

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

---

Latex:


\mforall{}[eo,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-forward-loc"  0  THENA  Auto)
  THEN  (RWO  "eo-forward-less"  0  THENA  Auto)
  THEN  EqCD)

---

Home Index