---

Step * 1 of Lemma bounded-above-strict


1. [A] : Set(ℝ)
2. b : ℝ
3. A ≤ b
⊢ ∃b:ℝ. A < b
BY
{ ((Assert r0 < (r1/r(1000)) BY Auto) THEN nRAdd ⌜b⌝ (-1)⋅ THEN InstConcl [⌜(r1/r(1000)) + b⌝]⋅ THEN Auto)⋅ }

1
1. [A] : Set(ℝ)
2. b : ℝ
3. A ≤ b
4. b < ((r1/r(1000)) + b)
⊢ A < (r1/r(1000)) + b

---

Latex:

---

Latex:

1.  [A]  :  Set(\mBbbR{})
2.  b  :  \mBbbR{}
3.  A  \mleq{}  b
\mvdash{}  \mexists{}b:\mBbbR{}.  A  <  b


By

---

Latex:
((Assert  r0  <  (r1/r(1000))  BY
                Auto)
  THEN  nRAdd  \mkleeneopen{}b\mkleeneclose{}  (-1)\mcdot{}
  THEN  InstConcl  [\mkleeneopen{}(r1/r(1000))  +  b\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index