---

Step * of Lemma eo-forward-base-pred

∀[eo,e,x:Top].  (pred1(x) ~ pred1(x))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``es-base-pred eo-forward eo-restrict`` 0 THEN Fold `es-base-pred` 0 THEN Auto) }

---

Latex:


\mforall{}[eo,e,x:Top].    (pred1(x)  \msim{}  pred1(x))


By

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

---

Home Index