---

Step * 13 1 of Lemma r2-basic-geo-axioms


∀a,b,c,y:ℝ^2.
  ((r2-left(a;b;c) ∨ r2-left(a;c;b))
  ⇒ (d(y;y) < d(y;b))
  ⇒ (¬(r2-left(y;a;b) ∨ r2-left(y;b;a)))
  ⇒ (r2-left(y;b;c) ∨ r2-left(y;c;b)))
BY
{ ((RWO  "r2-left-or-right--pos-angle" 0 THENA Auto)
   THEN (InstLemma `rv-pos-angle-implies` [⌜2⌝]⋅ THENA Auto)
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN BHyp -1
   THEN Auto
   THEN Try ((RWO "real-vec-sep-iff2" 0 THEN Auto))) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. y : ℝ^2
5. rv-pos-angle(2;a;b;c)
6. d(y;y) < d(y;b)
7. ¬rv-pos-angle(2;y;a;b)
8. rv-pos-angle(2;c;b;a)
9. rv-pos-angle(2;c;a;b)
10. a ≠ c
11. ¬a-b-c
12. ∀z:ℝ^2. (z ≠ b ⇒ (¬rv-pos-angle(2;a;b;z)) ⇒ rv-pos-angle(2;z;b;c))
⊢ ¬rv-pos-angle(2;a;b;y)

---

Latex:

---

Latex:

\mforall{}a,b,c,y:\mBbbR{}\^{}2.
    ((r2-left(a;b;c)  \mvee{}  r2-left(a;c;b))
    {}\mRightarrow{}  (d(y;y)  <  d(y;b))
    {}\mRightarrow{}  (\mneg{}(r2-left(y;a;b)  \mvee{}  r2-left(y;b;a)))
    {}\mRightarrow{}  (r2-left(y;b;c)  \mvee{}  r2-left(y;c;b)))


By

---

Latex:
((RWO    "r2-left-or-right--pos-angle"  0  THENA  Auto)
  THEN  (InstLemma  `rv-pos-angle-implies`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  BHyp  -1
  THEN  Auto
  THEN  Try  ((RWO  "real-vec-sep-iff2"  0  THEN  Auto)))

---

Home Index