---

Step * of Lemma member-es-interval

∀es:EO. ∀e,e',ev:E.  ((ev ∈ [e, e']) ⇐⇒ e ≤loc ev  ∧ ev ≤loc e' )
BY
{ (UnivCD THENA Auto) }

1
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' 

---

Latex:


\mforall{}es:EO.  \mforall{}e,e',ev:E.    ((ev  \mmember{}  [e,  e'])  \mLeftarrow{}{}\mRightarrow{}  e  \mleq{}loc  ev    \mwedge{}  ev  \mleq{}loc  e'  )


By

(UnivCD  THENA  Auto)

---

Home Index