---

Step * of Lemma member-es-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  <loc  ev)  \mwedge{}  (ev  <loc  e'))


By

(UnivCD  THENA  Auto)

---

Home Index