---

Step * 2 1 of Lemma i-finite-iff-bounded

.....assertion..... 
1. I : Interval
2. a : ℝ
3. b : ℝ
4. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
⊢ (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
BY
{ (D 0 THEN (D 0 THENA Auto)) }

1
1. I : Interval
2. a : ℝ
3. b : ℝ
4. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
5. (b + r1) ≤ b
⊢ False

2
1. I : Interval
2. a : ℝ
3. b : ℝ
4. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
5. a ≤ (a - r1)
⊢ False

---

Latex:

---

Latex:
.....assertion..... 
1.  I  :  Interval
2.  a  :  \mBbbR{}
3.  b  :  \mBbbR{}
4.  \mforall{}[r:\mBbbR{}].  a\mleq{}r\mleq{}b  supposing  r  \mmember{}  I
\mvdash{}  (\mneg{}((b  +  r1)  \mleq{}  b))  \mwedge{}  (\mneg{}(a  \mleq{}  (a  -  r1)))


By

---

Latex:
(D  0  THEN  (D  0  THENA  Auto))

---

Home Index