---

Step * of Lemma rleq_weakening_rless

∀[x,y:ℝ].  x ≤ y supposing x < y
BY
{ (Auto
   THEN BLemma `rleq-iff4`
   THEN Auto
   THEN (SupposeNot THEN Auto)
   THEN (Assert y < x BY
               (With ⌜n⌝ (D 0)⋅ THEN Auto))
   THEN Assert ⌜False⌝⋅
   THEN Auto) }

1
.....assertion..... 
1. x : ℝ
2. y : ℝ
3. x < y
4. n : ℕ+@i
5. ¬((x n) ≤ ((y n) + 4))
6. y < x
⊢ False

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    x  \mleq{}  y  supposing  x  <  y


By

---

Latex:
(Auto
  THEN  BLemma  `rleq-iff4`
  THEN  Auto
  THEN  (SupposeNot  THEN  Auto)
  THEN  (Assert  y  <  x  BY
                          (With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index