---

Step * 1 of Lemma strict-upper-bound_functionality


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
BY
{ (RWO "4<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Set(\mBbbR{})@i'
2.  b  :  \mBbbR{}@i
3.  c  :  \mBbbR{}@i
4.  b  \mleq{}  c
5.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  A)  {}\mRightarrow{}  (x  <  b))@i
6.  x  :  \mBbbR{}@i
7.  x  \mmember{}  A@i
\mvdash{}  x  <  c


By

---

Latex:
(RWO  "4<"  0  THEN  Auto)

---

Home Index