---

Step * of Lemma member-es-le-before2

∀es:EO. ∀e:E. ∀e':{a:E| loc(a) = loc(e) ∈ Id} .  ((e' ∈ ≤loc(e)) ⇐⇒ e' ≤loc e )
BY
{ (InstLemma `member-es-le-before` [] THEN RepeatFor 6 (ParallelLast') THEN Auto) }

---

Latex:


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


By

(InstLemma  `member-es-le-before`  []  THEN  RepeatFor  6  (ParallelLast')  THEN  Auto)

---

Home Index