---

Step * of Lemma es-interval-open-interval

∀[es:EO]. ∀[e,e':E].  [e', e] = (if e' <loc e then [e'] else [] fi  @ (e', e) @ [e]) ∈ (E List) supposing e' ≤loc e 
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀es:EO. ∀e,e':E.  (e' ≤loc e  ⇒ ([e', e] = (if e' <loc e then [e'] else [] fi  @ (e', e) @ [e]) ∈ (E List)))

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].
    [e',  e]  =  (if  e'  <loc  e  then  [e']  else  []  fi    @  (e',  e)  @  [e])  supposing  e'  \mleq{}loc  e 


By

(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index