---

Step * of Lemma rbinop_wf

∀[op:ℤ]. ∀[p,q:ℝ].  rbinop(op;p;q) ∈ ℝ supposing ((op = 6 ∈ ℤ) ⇒ q ≠ r0) ∧ ((op = 10 ∈ ℤ) ⇒ (r0 < p))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[op:\mBbbZ{}].  \mforall{}[p,q:\mBbbR{}].    rbinop(op;p;q)  \mmember{}  \mBbbR{}  supposing  ((op  =  6)  {}\mRightarrow{}  q  \mneq{}  r0)  \mwedge{}  ((op  =  10)  {}\mRightarrow{}  (r0  <  p))


By

---

Latex:
ProveWfLemma

---

Home Index