---

Step * of Lemma totally-bounded-sup

∀[A:Set(ℝ)]. (totally-bounded(A) ⇒ (∃b:ℝ. sup(A) = b))
BY
{ (Auto
   THEN BLemma `least-upper-bound`
   THEN Auto
   THEN Try ((BLemma `totally-bounded-implies-nonvoid` THEN Auto))
   THEN Try ((BLemma `totally-bounded-bounded-above` THEN Auto))) }

1
1. [A] : Set(ℝ)
2. totally-bounded(A)
3. x : ℝ
4. y : ℝ
5. x < y
⊢ (∃a:ℝ. ((a ∈ A) ∧ (x < a))) ∨ A ≤ y

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  (totally-bounded(A)  {}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  sup(A)  =  b))


By

---

Latex:
(Auto
  THEN  BLemma  `least-upper-bound`
  THEN  Auto
  THEN  Try  ((BLemma  `totally-bounded-implies-nonvoid`  THEN  Auto))
  THEN  Try  ((BLemma  `totally-bounded-bounded-above`  THEN  Auto)))

---

Home Index