---

Step * of Lemma rv-between_functionality3

∀n:ℕ. ∀a1,a2,b1,b2,c1,c2:ℝ^n.  ((¬a1 ≠ a2) ⇒ (¬b1 ≠ b2) ⇒ (¬c1 ≠ c2) ⇒ a1-b1-c1 ⇒ a2-b2-c2)
BY
{ (InstLemma `rv-between_functionality2` [] THEN RepeatFor 10 ((ParallelLast' THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a1,a2,b1,b2,c1,c2:\mBbbR{}\^{}n.    ((\mneg{}a1  \mneq{}  a2)  {}\mRightarrow{}  (\mneg{}b1  \mneq{}  b2)  {}\mRightarrow{}  (\mneg{}c1  \mneq{}  c2)  {}\mRightarrow{}  a1-b1-c1  {}\mRightarrow{}  a2-b2-c2)


By

---

Latex:
(InstLemma  `rv-between\_functionality2`  []  THEN  RepeatFor  10  ((ParallelLast'  THENA  Auto))  THEN  Auto)

---

Home Index