---

Step * of Lemma es-rank_property-base

∀[es:EO]. ∀[e1,e2:es-base-E(es)].  es-rank(es;e1) < es-rank(es;e2) supposing (e1 < e2)
BY
{ Intros }

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

2
1. es : EO
2. e1 : es-base-E(es)
3. e2 : es-base-E(es)
⊢ (e1 < e2) = (e1 < e2) ∈ Type

---

Latex:


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


By

Intros

---

Home Index