---

Step * of Lemma rv-be-symmetry

∀n:ℕ. ∀a,b,c:ℝ^n.  (a_b_c ⇒ c_b_a)
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN Auto THEN Try ((BLemma `real-vec-sep-symmetry` THEN Auto))) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. c ≠ b
6. b ≠ a
7. ¬c-b-a
8. a ≠ b
9. b ≠ c
⊢ ¬a-b-c

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (a\_b\_c  {}\mRightarrow{}  c\_b\_a)


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  Try  ((BLemma  `real-vec-sep-symmetry`  THEN  Auto)))

---

Home Index