---

Step * 1 of Lemma es-rank_property-base


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)
BY
{ ((InstLemma `event_ordering_properties` [⌈es⌉]⋅ THENA Auto) THEN D -1 THEN BackThruSomeHyp THEN Auto) }

---

Latex:



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


By

((InstLemma  `event\_ordering\_properties`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index