---

Step * of Lemma es-interval-last

∀[es:EO]. ∀[e2,e1:E].  last([e1, e2]) ~ e2 supposing e1 ≤loc e2 
BY
{ (UnivCD THENA Auto) }

1
1. es : EO
2. e2 : E
3. e1 : E
4. e1 ≤loc e2 
⊢ last([e1, e2]) ~ e2

---

Latex:


\mforall{}[es:EO].  \mforall{}[e2,e1:E].    last([e1,  e2])  \msim{}  e2  supposing  e1  \mleq{}loc  e2 


By

(UnivCD  THENA  Auto)

---

Home Index