---

Step * of Lemma eo-forward-less

∀[eo,e,e1,e2:Top].  ((e1 < e2) ~ (e1 < e2))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``es-causl eo-forward eo-restrict`` 0 THEN Fold `es-causl` 0 THEN Auto) }

---

Latex:


\mforall{}[eo,e,e1,e2:Top].    ((e1  <  e2)  \msim{}  (e1  <  e2))


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-causl  eo-forward  eo-restrict``  0
  THEN  Fold  `es-causl`  0
  THEN  Auto)

---

Home Index