---

Step * of Lemma eo-forward-causl

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

---

Latex:


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


By

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

---

Home Index