---

Step * of Lemma rpositive-rless

∀[x:ℝ]. (r0 < x ⇐⇒ rpositive(x))
BY
{ (RepUR ``rless int-to-real rpositive`` 0 THEN Auto THEN ParallelLast THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (r0  <  x  \mLeftarrow{}{}\mRightarrow{}  rpositive(x))


By

---

Latex:
(RepUR  ``rless  int-to-real  rpositive``  0  THEN  Auto  THEN  ParallelLast  THEN  Auto')

---

Home Index