---

Step * 1 of Lemma es-rank_le


1. es : EO
2. e1 : E
3. e2 : E
4. (e1 < e2)
⊢ es-rank(es;e1) ≤ es-rank(es;e2)
BY
{ (FLemma `es-rank_property` [-1] THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e1  :  E
3.  e2  :  E
4.  (e1  <  e2)
\mvdash{}  es-rank(es;e1)  \mleq{}  es-rank(es;e2)


By

(FLemma  `es-rank\_property`  [-1]  THEN  Auto)

---

Home Index