---

Step * 1 1 of Lemma totally-bounded-inf

.....assertion..... 
1. [A] : Set(ℝ)
2. totally-bounded(A)
⊢ ∃b:ℝ. sup(-(A)) = b
BY
{ (BLemma `totally-bounded-sup` THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  Set(\mBbbR{})
2.  totally-bounded(A)
\mvdash{}  \mexists{}b:\mBbbR{}.  sup(-(A))  =  b


By

---

Latex:
(BLemma  `totally-bounded-sup`  THEN  Auto)

---

Home Index