---

Step * of Lemma rless-witness_wf

∀[x,y:ℝ]. ∀[p:x < y].  (rless-witness(x;y;p) ∈ ℕ+)
BY
{ (Unfold `rless-witness` 0 THEN RepeatFor 2 (Auto)) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].  \mforall{}[p:x  <  y].    (rless-witness(x;y;p)  \mmember{}  \mBbbN{}\msupplus{})


By

---

Latex:
(Unfold  `rless-witness`  0  THEN  RepeatFor  2  (Auto))

---

Home Index