---

Step * of Lemma rmax-nonneg

∀[x,y:ℝ].  rnonneg(rmax(x;y)) supposing rnonneg(x) ∨ rnonneg(y)
BY
{ (Auto THEN Repeat (MoveToConcl (-1))) }

1
∀x,y:ℝ.  ((rnonneg(x) ∨ rnonneg(y)) ⇒ rnonneg(rmax(x;y)))

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    rnonneg(rmax(x;y))  supposing  rnonneg(x)  \mvee{}  rnonneg(y)


By

---

Latex:
(Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index