---

Step * of Lemma es-base-pred_wf

∀[the_es:EO]. ∀[e:es-base-E(the_es)].  (pred1(e) ∈ es-base-E(the_es))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN D 1
   THEN (DRecord 1⋅ THENA Auto)
   THEN All (RepUR ``es-base-pred es-base-E``)
   THEN Auto) }

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e:es-base-E(the$_{es}$)].    (pred1(e)  \mmember{}  e\000Cs-base-E(the$_{es}$))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  1
  THEN  (DRecord  1\mcdot{}  THENA  Auto)
  THEN  All  (RepUR  ``es-base-pred  es-base-E``)
  THEN  Auto)

---

Home Index