---

Step * of Lemma hd-es-interval

∀[es:EO]. ∀[e,e':E].  hd([e, e']) = e ∈ E supposing e ≤loc e' 
BY
{ (Auto THEN AssertBY (e ∈ [e, e'])    (BLemma `member-es-interval` THEN Auto)⋅) }

1
1. es : EO
2. e : E
3. e' : E
4. e ≤loc e' 
5. (e ∈ [e, e'])
⊢ hd([e, e']) = e ∈ E

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    hd([e,  e'])  =  e  supposing  e  \mleq{}loc  e' 


By

(Auto  THEN  AssertBY  (e  \mmember{}  [e,  e'])        (BLemma  `member-es-interval`  THEN  Auto)\mcdot{})

---

Home Index