---

Step * of Lemma es-fix-unique

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:E(X) ─→ E(X)].
  ∀[a,e:E(X)].  (f**(e) = a ∈ E(X)) supposing (((f a) = a ∈ E) and a is f*(e)) supposing ∀x:E(X). f x c≤ x
BY
{ Auto }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:E(X)  {}\mrightarrow{}  E(X)].
    \mforall{}[a,e:E(X)].    (f**(e)  =  a)  supposing  (((f  a)  =  a)  and  a  is  f*(e))  supposing  \mforall{}x:E(X).  f  x  c\mleq{}  x


By

Auto

---

Home Index