---

Step * of Lemma sq_stable__es-causl

∀[the_es:EO]. ∀[e,e':E].  SqStable((e < e'))
BY
{ (Auto THEN D 1 THEN (DRecord 1 THENA Auto) THEN All (RepUR ``es-E es-causl``) THEN Auto) }

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e,e':E].    SqStable((e  <  e'))


By

(Auto  THEN  D  1  THEN  (DRecord  1  THENA  Auto)  THEN  All  (RepUR  ``es-E  es-causl``)  THEN  Auto)

---

Home Index