---

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

.....antecedent..... 
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. e ≤loc e' @i
⊢ ¬([e, e'] = [] ∈ (E List))
BY
{ (AssertBY ⌈(e ∈ [e, e'])⌉
   (RWO "member-es-interval" 0 THEN Auto))⋅ }

1
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))

---

Latex:


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


By

(AssertBY  \mkleeneopen{}(e  \mmember{}  [e,  e'])\mkleeneclose{}
      (RWO  "member-es-interval"  0  THEN  Auto))\mcdot{}

---

Home Index