---

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


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' 
BY
{ (ExRepD THEN (RWO "member-es-interval" (-1)) THEN Auto) }

---

Latex:



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


By

(ExRepD  THEN  (RWO  "member-es-interval"  (-1))  THEN  Auto)

---

Home Index