---

Step * of Lemma rless-ibs

∀x,y:ℝ.
  ∃s:IBS
   ((x < y ⇐⇒ ∃n:ℕ. ((s n) = 1 ∈ ℤ))
   ∧ (∀n:ℕ. (((s n) = 0 ∈ ℤ) ⇒ (((y < x) ∧ (∀m:ℕ. ((s m) = 0 ∈ ℤ))) ∨ (|x - y| ≤ (r(4)/r(n + 1)))))))
BY
{ (InstLemma `rless_ibs_property` [] THEN RepeatFor 2 (ParallelLast') THEN D 0 With ⌜rless_ibs(x;y)⌝  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.
    \mexists{}s:IBS
      ((x  <  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((s  n)  =  1))
      \mwedge{}  (\mforall{}n:\mBbbN{}.  (((s  n)  =  0)  {}\mRightarrow{}  (((y  <  x)  \mwedge{}  (\mforall{}m:\mBbbN{}.  ((s  m)  =  0)))  \mvee{}  (|x  -  y|  \mleq{}  (r(4)/r(n  +  1)))))))


By

---

Latex:
(InstLemma  `rless\_ibs\_property`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  D  0  With  \mkleeneopen{}rless\_ibs(x;y)\mkleeneclose{} 
  THEN  Auto)

---

Home Index