---

Step * of Lemma es-interval-length-one-one

∀[es:EO]. ∀[d,b,a:E].  (b = d ∈ E) supposing ((||[a, b]|| = ||[a, d]|| ∈ ℤ) and a ≤loc d  and a ≤loc b )
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀es:EO. ∀d,b,a:E.  (a ≤loc b  ⇒ a ≤loc d  ⇒ (||[a, b]|| = ||[a, d]|| ∈ ℤ) ⇒ (b = d ∈ E))

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[d,b,a:E].    (b  =  d)  supposing  ((||[a,  b]||  =  ||[a,  d]||)  and  a  \mleq{}loc  d    and  a  \mleq{}loc  b  )


By

---

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

---

Home Index