---

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


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. 0 < ||[e, e']||@i
⊢ e ≤loc e' 
BY
{ ((InstLemma `member_exists` [⌈E⌉; ⌈[e, e']⌉])⋅ THEN Auto) }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. 0 < ||[e, e']||@i
5. ∃x:E. (x ∈ [e, e'])
⊢ e ≤loc e' 

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  0  <  ||[e,  e']||@i
\mvdash{}  e  \mleq{}loc  e' 


By

((InstLemma  `member\_exists`  [\mkleeneopen{}E\mkleeneclose{};  \mkleeneopen{}[e,  e']\mkleeneclose{}])\mcdot{}  THEN  Auto)

---

Home Index