---

Step * of Lemma rless-content

∀[x:ℝ]. ∀[y:{y:ℝ| x < y} ].  (rlessw(x;y) ∈ x < y)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[y:\{y:\mBbbR{}|  x  <  y\}  ].    (rlessw(x;y)  \mmember{}  x  <  y)


By

---

Latex:
Auto

---

Home Index