---

Step * of Lemma r2-not-left-right-iff

∀a,b,c:ℝ^2.  (¬(r2-left(a;b;c) ∨ r2-left(a;c;b)) ⇐⇒ ¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b)))
BY
{ ((InstLemma `r2-not-left-right` [] THEN RepeatFor 3 (ParallelLast'))
   THEN (RWO "rv-T-iff" (-1) THENA Auto)
   THEN Fold `rv-be` (-1)
   THEN Auto
   THEN (D 0 THENA Auto)) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. (¬r2-left(a;b;c)) ⇒ (¬r2-left(a;c;b)) ⇒ (¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b)))
5. ¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b))
6. r2-left(a;b;c) ∨ r2-left(a;c;b)
⊢ False

---

Latex:

---

Latex:
\mforall{}a,b,c:\mBbbR{}\^{}2.    (\mneg{}(r2-left(a;b;c)  \mvee{}  r2-left(a;c;b))  \mLeftarrow{}{}\mRightarrow{}  \mneg{}((\mneg{}a\_b\_c)  \mwedge{}  (\mneg{}b\_c\_a)  \mwedge{}  (\mneg{}c\_a\_b)))


By

---

Latex:
((InstLemma  `r2-not-left-right`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  (RWO  "rv-T-iff"  (-1)  THENA  Auto)
  THEN  Fold  `rv-be`  (-1)
  THEN  Auto
  THEN  (D  0  THENA  Auto))

---

Home Index