---

Step * of Lemma es-pplus-alle-between2

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[Q:{e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ]. ([e1,e2]~([a,b].∀e∈[a,b].Q[e])+ ⇐⇒ e1 ≤loc e2  ∧ ∀e∈[e1,e2].Q[e])
BY
{ ((D 0 THENA Auto)
   THEN Auto
   THEN Auto
   THEN Try (((FLemma `es-pplus-le` [(-1)]) THEN Auto))
   THEN Try ((BLemma `es-pplus-trivial` THEN Auto))) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [Q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [e1,e2]~([a,b].∀e∈[a,b].Q[e])+@i
6. e1 ≤loc e2 
⊢ ∀e∈[e1,e2].Q[e]

---

Latex:


\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
    \mforall{}[Q:\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}]
        ([e1,e2]\msim{}([a,b].\mforall{}e\mmember{}[a,b].Q[e])+  \mLeftarrow{}{}\mRightarrow{}  e1  \mleq{}loc  e2    \mwedge{}  \mforall{}e\mmember{}[e1,e2].Q[e])


By

((D  0  THENA  Auto)
  THEN  Auto
  THEN  Auto
  THEN  Try  (((FLemma  `es-pplus-le`  [(-1)])  THEN  Auto))
  THEN  Try  ((BLemma  `es-pplus-trivial`  THEN  Auto)))

---

Home Index