---

Step * of Lemma rless_transitivity

∀x,y,z:ℝ.  ((x < y) ⇒ (y < z) ⇒ (x < z))
BY
{ (Auto THEN (All (RWO "rless-iff4") THEN Auto) THEN ExRepD) }

1
1. x : ℝ@i
2. y : ℝ@i
3. z : ℝ@i
4. n1 : ℕ+
5. ∀m:{n1...}. (x m) + 4 < y m
6. n : ℕ+
7. ∀m:{n...}. (y m) + 4 < z m
⊢ ∃n:ℕ+. ∀m:{n...}. (x m) + 4 < z m

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (All  (RWO  "rless-iff4")  THEN  Auto)  THEN  ExRepD)

---

Home Index