---

Step * of Lemma trivial-rless-radd

∀a,d:ℝ.  (uiff(a < (a + d);r0 < d) ∧ uiff(a < (d + a);r0 < d))
BY
{ (Auto THEN Unhide THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,d:\mBbbR{}.    (uiff(a  <  (a  +  d);r0  <  d)  \mwedge{}  uiff(a  <  (d  +  a);r0  <  d))


By

---

Latex:
(Auto  THEN  Unhide  THEN  Auto)

---

Home Index