---

Step * 1 2 of Lemma totally-bounded-inf


1. [A] : Set(ℝ)
2. totally-bounded(A)
3. ∃b:ℝ. sup(-(A)) = b
⊢ ∃b:ℝ. sup(-(A)) = -(b)
BY
{ (D (-1) THEN InstConcl [⌜-(b)⌝] ⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(D  (-1)  THEN  InstConcl  [\mkleeneopen{}-(b)\mkleeneclose{}]  \mcdot{}  THEN  Auto)

---

Home Index