---

Step * of Lemma member-es-closed-open-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  <loc  e'))


By

(UnivCD  THENA  Auto)

---

Home Index