---

Step * of Lemma member-es-le-before

∀es:EO. ∀e,e':E.  ((e' ∈ ≤loc(e)) ⇐⇒ e' ≤loc e )
BY
{ ((UnivCD
    THENM Unfold `es-le-before` 0
    THENM RWO "member_append" 0
    THENM RWO "member-es-before" 0
    THENM RWO "member_singleton" 0
    THENM Fold `es-le` 0)
   THEN Auto
   ) }

---

Latex:


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


By

((UnivCD
    THENM  Unfold  `es-le-before`  0
    THENM  RWO  "member\_append"  0
    THENM  RWO  "member-es-before"  0
    THENM  RWO  "member\_singleton"  0
    THENM  Fold  `es-le`  0)
  THEN  Auto
  )

---

Home Index