---

Step * of Lemma stable__rleq

∀[x,y:ℝ].  Stable{x ≤ y}
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RWO "rleq-iff4" 0
   THEN Auto
   THEN (SupposeNot THENA Auto)
   THEN D 3
   THEN (D 0 THENA Auto)
   THEN (RWO "rleq-iff4" (-1) THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
4. ¬((x n) ≤ ((y n) + 4))
5. ∀n:ℕ+. ((x n) ≤ ((y n) + 4))
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RWO  "rleq-iff4"  0
  THEN  Auto
  THEN  (SupposeNot  THENA  Auto)
  THEN  D  3
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "rleq-iff4"  (-1)  THENA  Auto))

---

Home Index