---

Step * 1 1 1 of Lemma member-es-interval


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
5. e ≤loc ev @i
6. ev ≤loc e' @i
⊢ (ev <loc e') ∨ (ev = e' ∈ E) ∨ False
BY
{ ((Unfold `es-le` (-1)) THEN (ParallelOp (-1))) }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
5. e ≤loc ev @i
6. ev = e' ∈ E@i
⊢ (ev = e' ∈ E) ∨ False

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  ev  :  E@i
5.  e  \mleq{}loc  ev  @i
6.  ev  \mleq{}loc  e'  @i
\mvdash{}  (ev  <loc  e')  \mvee{}  (ev  =  e')  \mvee{}  False


By

((Unfold  `es-le`  (-1))  THEN  (ParallelOp  (-1)))

---

Home Index