---

Step * of Lemma rless-cases

∀x,y:ℝ.  ((x < y) ⇒ (∀z:ℝ. ((x < z) ∨ (z < y))))
BY
{ Extract of Obid: rless-cases-proof
  normalizes to:
  
  λx,y,n,z. rless-case(x;y;n;z)
  
  not unfolding  
  finishing with (Unfold `rless-case` 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  rless-cases-proof
normalizes  to:

\mlambda{}x,y,n,z.  rless-case(x;y;n;z)

not  unfolding   
finishing  with  (Unfold  `rless-case`  0  THEN  Auto)

---

Home Index