---

Step * of Lemma rmin-max-cases

∀a,b:ℝ.  (a ≠ b ⇒ (((rmin(a;b) = a) ∧ (rmax(a;b) = b)) ∨ ((rmin(a;b) = b) ∧ (rmax(a;b) = a))))
BY
{ (Auto THEN Unfold `rneq` -1 THEN ParallelLast THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    (a  \mneq{}  b  {}\mRightarrow{}  (((rmin(a;b)  =  a)  \mwedge{}  (rmax(a;b)  =  b))  \mvee{}  ((rmin(a;b)  =  b)  \mwedge{}  (rmax(a;b)  =  a))))


By

---

Latex:
(Auto  THEN  Unfold  `rneq`  -1  THEN  ParallelLast  THEN  EAuto  1)

---

Home Index