---

Step * of Lemma es-causl_wf

∀[the_es:EO]. ∀[e,e':E].  ((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].    ((e  <  e')  \mmember{}  \mBbbP{})


By

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

---

Home Index