---

Step * of Lemma member-es-hist

∀[Info:Type]. ∀es:EO+(Info). ∀e1,e2:E. ∀t:Info.  ((t ∈ es-hist(es;e1;e2)) ⇐⇒ ∃e∈[e1,e2].t = info(e) ∈ Info)
BY
{ ((UnivCD THENA Auto)
   THEN Unfolds ``es-hist existse-between2`` 0
   THEN RWW "member_map member-es-interval" 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:


\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.  \mforall{}t:Info.    ((t  \mmember{}  es-hist(es;e1;e2))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e\mmember{}[e1,e2].t  =  info(e))


By

((UnivCD  THENA  Auto)
  THEN  Unfolds  ``es-hist  existse-between2``  0
  THEN  RWW  "member\_map  member-es-interval"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index