Step
*
1
of Lemma
es-interval-length-one-one
∀es:EO. ∀d,b,a:E. (a ≤loc b
⇒ a ≤loc d
⇒ (||[a, b]|| = ||[a, d]|| ∈ ℤ)
⇒ (b = d ∈ E))
BY
{ ((((D 0 THENA Auto) THEN LocLessInd) THENA Auto) THEN LocLessInd THEN 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)
⇒ (∀b,a:E. (a ≤loc b
⇒ a ≤loc k
⇒ (||[a, b]|| = ||[a, k]|| ∈ ℤ)
⇒ (b = k ∈ E))))@i
5. WellFnd{i}(E;x,y.(x <loc y))
6. j1 : E@i
7. ∀k:E. ((k <loc j1)
⇒ (∀a:E. (a ≤loc k
⇒ a ≤loc j
⇒ (||[a, k]|| = ||[a, j]|| ∈ ℤ)
⇒ (k = j ∈ E))))@i
8. a : E@i
9. a ≤loc j1 @i
10. a ≤loc j @i
11. ||[a, j1]|| = ||[a, j]|| ∈ ℤ@i
⊢ j1 = j ∈ E
Latex:
\mforall{}es:EO. \mforall{}d,b,a:E. (a \mleq{}loc b {}\mRightarrow{} a \mleq{}loc d {}\mRightarrow{} (||[a, b]|| = ||[a, d]||) {}\mRightarrow{} (b = d))
By
((((D 0 THENA Auto) THEN LocLessInd) THENA Auto) THEN LocLessInd THEN Auto)
Home
Index