---

Step * of Lemma rstar-rleq

∀[x,y:ℝ].  ((x)* ≤ (y)* ⇐⇒ x ≤ y)
BY
{ Auto }

1
1. x : ℝ
2. y : ℝ
3. (x)* ≤ (y)*
⊢ x ≤ y

2
1. [x] : ℝ
2. [y] : ℝ
3. x ≤ y
⊢ (x)* ≤ (y)*

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    ((x)*  \mleq{}  (y)*  \mLeftarrow{}{}\mRightarrow{}  x  \mleq{}  y)


By

---

Latex:
Auto

---

Home Index