---

Step * of Lemma es-causle-interface-retraction

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀f:E(X) ─→ E(X).  ((∀x:E(X). f x c≤ x) ⇒ retraction(E(X);f))
BY
{ (Auto THEN UsingVars [`es'] (BLemma `es-causle-retraction`) THEN Auto) }

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}f:E(X)  {}\mrightarrow{}  E(X).    ((\mforall{}x:E(X).  f  x  c\mleq{}  x)  {}\mRightarrow{}  retraction(E(X);f))


By

(Auto  THEN  UsingVars  [`es']  (BLemma  `es-causle-retraction`)  THEN  Auto)

---

Home Index