---

Step * of Lemma strict-upper-bound_functionality

∀A:Set(ℝ). ∀b,c:ℝ.  {A < b ⇒ A < c} supposing b ≤ c
BY
{ (Unfolds ``strict-upper-bound guard`` 0 THEN Auto) }

1
1. A : Set(ℝ)@i'
2. b : ℝ@i
3. c : ℝ@i
4. b ≤ c
5. ∀x:ℝ. ((x ∈ A) ⇒ (x < b))@i
6. x : ℝ@i
7. x ∈ A@i
⊢ x < c

---

Latex:

---

Latex:
\mforall{}A:Set(\mBbbR{}).  \mforall{}b,c:\mBbbR{}.    \{A  <  b  {}\mRightarrow{}  A  <  c\}  supposing  b  \mleq{}  c


By

---

Latex:
(Unfolds  ``strict-upper-bound  guard``  0  THEN  Auto)

---

Home Index