---

Step * of Lemma es-subinterval

∀es:EO. ∀e2,e1:E.  (e1 ≤loc e2  ⇒ (∀n:ℕ. (∃e∈(e1,e2].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, e2]|| and 0 < n))\000C)
BY
{ (((D 0 THENA Auto) THEN LocLessInd) THENA Auto) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E
     ((k <loc j)
     ⇒ (∀e1:E. (e1 ≤loc k  ⇒ (∀n:ℕ. (∃e∈(e1,k].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, k]|| and 0 < n)))))@i
⊢ ∀e1:E. (e1 ≤loc j  ⇒ (∀n:ℕ. (∃e∈(e1,j].||[e1, pred(e)]|| = n ∈ ℤ) supposing (n < ||[e1, j]|| and 0 < n)))

---

Latex:


\mforall{}es:EO.  \mforall{}e2,e1:E.
    (e1  \mleq{}loc  e2    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (\mexists{}e\mmember{}(e1,e2].||[e1,  pred(e)]||  =  n)  supposing  (n  <  ||[e1,  e2]||  and  0  <  n)))


By

(((D  0  THENA  Auto)  THEN  LocLessInd)  THENA  Auto)

---

Home Index