---

Step * of Lemma es-closed-open-interval-decomp-member

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2,e:E].  [e1;e2) = ([e1;e) @ [e;e2)) ∈ (E List) supposing (e ∈ [e1, e2])
BY
{ (Auto THEN (RW ListC (-1) THENA Auto) THEN BLemma `es-closed-open-interval-decomp-mem` THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2,e:E].    [e1;e2)  =  ([e1;e)  @  [e;e2))  supposing  (e  \mmember{}  [e1,  e2])


By

(Auto  THEN  (RW  ListC  (-1)  THENA  Auto)  THEN  BLemma  `es-closed-open-interval-decomp-mem`  THEN  Auto)

---

Home Index