---

Step * 1 of Lemma member-es-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-open-interval` 0 THEN RWO "member_filter" 0) THENM Reduce 0)
   THENM RWW "member-es-before assert-es-bless" 0
   )
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

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  <loc  ev)  \mwedge{}  (ev  <loc  e')


By

---

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

---

Home Index