---

Step * of Lemma member-es-le-before3

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

1
1. es : EO@i'
2. e : E@i
3. e' : {e':E| e' ≤loc e } @i
4. i : ℕ@i
5. i < ||≤loc(e)||@i
6. e' = ≤loc(e)[i] ∈ {e':E| e' ≤loc e } @i
⊢ e' = ≤loc(e)[i] ∈ E

2
1. es : EO@i'
2. e : E@i
3. e' : {e':E| e' ≤loc e } @i
4. e' ≤loc e @i
5. i : ℕ
6. i < ||≤loc(e)||
7. e' = ≤loc(e)[i] ∈ E
⊢ e' = ≤loc(e)[i] ∈ {e':E| e' ≤loc e } 

---

Latex:


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


By

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

---

Home Index