---

Step * of Lemma eo-strict-forward-less

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

---

Latex:


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


By

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

---

Home Index