---

Step * of Lemma rless-case_wf

∀[x,y:ℝ]. ∀[n:x < y]. ∀[z:ℝ].  (rless-case(x;y;n;z) ∈ (x < z) ∨ (z < y))
BY
{ (Auto
   THEN (Assert TERMOF{rless-cases:o, 1:l} ∈ ∀x,y:ℝ.  ((x < y) ⇒ (∀z:ℝ. ((x < z) ∨ (z < y)))) BY
               Auto)
   THEN Subst' rless-case(x;y;n;z) ~ TERMOF{rless-cases:o, 1:l} x y n z 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].  \mforall{}[n:x  <  y].  \mforall{}[z:\mBbbR{}].    (rless-case(x;y;n;z)  \mmember{}  (x  <  z)  \mvee{}  (z  <  y))


By

---

Latex:
(Auto
  THEN  (Assert  TERMOF\{rless-cases:o,  1:l\}  \mmember{}  \mforall{}x,y:\mBbbR{}.    ((x  <  y)  {}\mRightarrow{}  (\mforall{}z:\mBbbR{}.  ((x  <  z)  \mvee{}  (z  <  y))))  BY
                          Auto)
  THEN  Subst'  rless-case(x;y;n;z)  \msim{}  TERMOF\{rless-cases:o,  1:l\}  x  y  n  z  0
  THEN  Auto)

---

Home Index