---

Step * of Lemma rlessw_wf

∀x:ℝ. ∀y:{y:ℝ| x < y} .  (rlessw(x;y) ∈ x < y)
BY
{ ((UnivCD THENA Auto) THEN D -1 THEN (RWO "rless-iff4" (-1) THENA Auto)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. ∃n:ℕ+. ∀m:{n...}. (x m) + 4 < y m
⊢ rlessw(x;y) ∈ x < y

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  -1  THEN  (RWO  "rless-iff4"  (-1)  THENA  Auto))

---

Home Index