---

Step * of Lemma rleq-iff-rleq2

∀x,y:ℝ.  (x ≤ y ⇐⇒ rleq2(x;y))
BY
{ ((UnivCD THENA Auto) THEN (RWO "rleq-iff" 0 THENA Auto) THEN Fold `rleq2` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (x  \mleq{}  y  \mLeftarrow{}{}\mRightarrow{}  rleq2(x;y))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "rleq-iff"  0  THENA  Auto)  THEN  Fold  `rleq2`  0  THEN  Auto)

---

Home Index