---

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


∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
BY
{ (UnfoldGeoAbbreviations 0
   THEN (RWO "rv-congruent-iff2< real-vec-sep-iff2<" 0 THENA Auto)
   THEN Auto
   THEN (InstLemma `r2-upper-dimension` [⌜x⌝;⌜y⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto)) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. x : ℝ^2
5. y : ℝ^2
6. ax=ay
7. bx=by
8. cx=cy
9. x ≠ y
10. ¬(a ≠ b ∧ b ≠ c ∧ c ≠ a ∧ (¬a-b-c) ∧ (¬b-c-a) ∧ (¬c-a-b))
⊢ ¬(r2-left(a;b;c) ∨ r2-left(a;c;b))

---

Latex:

---

Latex:

\mforall{}a,b,c,x,y:Point.    (ax  \mcong{}  ay  {}\mRightarrow{}  bx  \mcong{}  by  {}\mRightarrow{}  cx  \mcong{}  cy  {}\mRightarrow{}  x  \#  y  {}\mRightarrow{}  (\mneg{}a  \#  bc))


By

---

Latex:
(UnfoldGeoAbbreviations  0
  THEN  (RWO  "rv-congruent-iff2<  real-vec-sep-iff2<"  0  THENA  Auto)
  THEN  Auto
  THEN  (InstLemma  `r2-upper-dimension`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index