---

Step * of Lemma es-rank-wf-base

∀[es:EO]. ∀[e:es-base-E(es)].  (es-rank(es;e) ∈ ℕ)
BY
{ ((UnivCD THENA Auto) THEN D 1 THEN (DRecord 1⋅ THENA Auto) THEN All (Fold `es-E`) THEN ProveWfLemma) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:es-base-E(es)].    (es-rank(es;e)  \mmember{}  \mBbbN{})


By

((UnivCD  THENA  Auto)  THEN  D  1  THEN  (DRecord  1\mcdot{}  THENA  Auto)  THEN  All  (Fold  `es-E`)  THEN  ProveWfLemma)

---

Home Index