---

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


∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)
BY
{ UnfoldGeoAbbreviations 0 }

1
∀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)))

---

Latex:

---

Latex:

\mforall{}a,b,c,y:Point.    (a  \#  bc  {}\mRightarrow{}  y  \#  b  {}\mRightarrow{}  (\mneg{}y  \#  ab)  {}\mRightarrow{}  y  \#  bc)


By

---

Latex:
UnfoldGeoAbbreviations  0

---

Home Index