---

Step * 1 1 1 of Lemma es-interval-non-zero


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. e ≤loc e' @i
5. (e ∈ [e, e'])
⊢ ¬([e, e'] = [] ∈ (E List))
BY
{ (D 0 THEN Auto THEN (HypSubst (-1) (-2)) THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  e  \mleq{}loc  e'  @i
5.  (e  \mmember{}  [e,  e'])
\mvdash{}  \mneg{}([e,  e']  =  [])


By

(D  0  THEN  Auto  THEN  (HypSubst  (-1)  (-2))  THEN  Auto)

---

Home Index