---

Step * of Lemma es-rank_property

∀[es:EO]. ∀[e1,e2:E].  es-rank(es;e1) < es-rank(es;e2) supposing (e1 < e2)
BY
{ ((UnivCD THENA Auto)⋅ THEN BLemma `es-rank_property-base` THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e1,e2:E].    es-rank(es;e1)  <  es-rank(es;e2)  supposing  (e1  <  e2)


By

((UnivCD  THENA  Auto)\mcdot{}  THEN  BLemma  `es-rank\_property-base`  THEN  Auto)

---

Home Index