---

Step * of Lemma es-rank_le

∀[es:EO]. ∀[e1,e2:E].  es-rank(es;e1) ≤ es-rank(es;e2) supposing e1 c≤ e2
BY
{ (Auto THEN D -1) }

1
1. es : EO
2. e1 : E
3. e2 : E
4. (e1 < e2)
⊢ es-rank(es;e1) ≤ es-rank(es;e2)

2
1. es : EO
2. e1 : E
3. e2 : E
4. e1 = e2 ∈ E
⊢ es-rank(es;e1) ≤ es-rank(es;e2)

---

Latex:


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


By

(Auto  THEN  D  -1)

---

Home Index