---

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


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
⊢ (ev ∈ [e;e')) ⇐⇒ e ≤loc ev  ∧ (ev <loc e')
BY
{ ((((Unfold `es-closed-open-interval` 0 THEN RWO "member_filter" 0) THENM Reduce 0)
   THENM RWW "member-es-before assert-es-ble" 0
   )
   THEN Reduce 0
   THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  ev  :  E@i
\mvdash{}  (ev  \mmember{}  [e;e'))  \mLeftarrow{}{}\mRightarrow{}  e  \mleq{}loc  ev    \mwedge{}  (ev  <loc  e')


By

((((Unfold  `es-closed-open-interval`  0  THEN  RWO  "member\_filter"  0)  THENM  Reduce  0)
  THENM  RWW  "member-es-before  assert-es-ble"  0
  )
  THEN  Reduce  0
  THEN  Auto)

---

Home Index