---

Step * of Lemma bounded-above-strict

∀[A:Set(ℝ)]. (bounded-above(A) ⇒ (∃b:ℝ. A < b))
BY
{ (Unfold `bounded-above` 0 THEN Auto THEN ExRepD) }

1
1. [A] : Set(ℝ)
2. b : ℝ
3. A ≤ b
⊢ ∃b:ℝ. A < b

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  (bounded-above(A)  {}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  A  <  b))


By

---

Latex:
(Unfold  `bounded-above`  0  THEN  Auto  THEN  ExRepD)

---

Home Index