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