---

Step * of Lemma rv-Tsep-alt'

∀n:ℕ. ∀a,b,c,d:ℝ^n.  ((¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ cd=uw))) ⇒ a ≠ b ⇒ c ≠ d)
BY
{ (InstLemma `rv-Tsep-alt` [] THEN RWO  "rv-T-iff" (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c,d:\mBbbR{}\^{}n.
    ((\mneg{}\mneg{}(\mexists{}u,v,w:\mBbbR{}\^{}n.  ((\mneg{}(u  \mneq{}  v  \mwedge{}  v  \mneq{}  w  \mwedge{}  (\mneg{}u-v-w)))  \mwedge{}  ab=uv  \mwedge{}  cd=uw)))  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  c  \mneq{}  d)


By

---

Latex:
(InstLemma  `rv-Tsep-alt`  []  THEN  RWO    "rv-T-iff"  (-1)  THEN  Auto)

---

Home Index