---

Step * 1 of Lemma sup-unique


1. A : Set(ℝ)
2. b : ℝ
3. c : ℝ
4. A ≤ b
5. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ ((b - e) < x))))
6. A ≤ c
7. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ A) ∧ ((c - e) < x))))
8. k : ℕ+
⊢ (b - c) ≤ (r1/r(k))
BY
{ (((InstHyp [⌜(r1/r(k))⌝] 5)⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert x ≤ c BY
               Auto)
   THEN ((RWO "-1" (-2)) THENA Auto)
   THEN (RWO "-2<" 0 THENA Auto)
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Set(\mBbbR{})
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  A  \mleq{}  b
5.  \mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  A)  \mwedge{}  ((b  -  e)  <  x))))
6.  A  \mleq{}  c
7.  \mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  A)  \mwedge{}  ((c  -  e)  <  x))))
8.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  (b  -  c)  \mleq{}  (r1/r(k))


By

---

Latex:
(((InstHyp  [\mkleeneopen{}(r1/r(k))\mkleeneclose{}]  5)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  x  \mleq{}  c  BY
                          Auto)
  THEN  ((RWO  "-1"  (-2))  THENA  Auto)
  THEN  (RWO  "-2<"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index