---

Step * of Lemma rless-cases1

∀x,y:ℝ.  ((x < y) ⇒ (∀z:ℝ. ((x < z) ∨ (z < y))))
BY
{ (Auto THEN ((InstLemma `radd-positive-implies` [⌜z - x⌝; ⌜y - z⌝])⋅ THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. x < y
4. z : ℝ
5. (r0 < (z - x)) ∨ (r0 < (y - z))
⊢ (x < z) ∨ (z < y)

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((x  <  y)  {}\mRightarrow{}  (\mforall{}z:\mBbbR{}.  ((x  <  z)  \mvee{}  (z  <  y))))


By

---

Latex:
(Auto  THEN  ((InstLemma  `radd-positive-implies`  [\mkleeneopen{}z  -  x\mkleeneclose{};  \mkleeneopen{}y  -  z\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index