---

Step * of Lemma real-has-value

∀[x:ℝ]. (x)↓
BY
{ (Auto THEN D 1) }

1
1. x : ℕ+ ⟶ ℤ
2. [%1] : regular-seq(x)
⊢ (x)↓

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (x)\mdownarrow{}


By

---

Latex:
(Auto  THEN  D  1)

---

Home Index