---

Step * 2 of Lemma es-rank_property-base


1. es : EO
2. e1 : es-base-E(es)
3. e2 : es-base-E(es)
⊢ (e1 < e2) = (e1 < e2) ∈ Type
BY
{ (Fold `member` 0 THEN BLemma `es-causl-wf-base` THEN Auto) }

---

Latex:



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


By

(Fold  `member`  0  THEN  BLemma  `es-causl-wf-base`  THEN  Auto)

---

Home Index