---

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


∀a,b,c:Point.  (ba>ac ⇒ b # c)
BY
{ (UnfoldGeoAbbreviations 0
   THEN Auto
   THEN (Assert d(b;a) ≤ (d(b;c) + d(c;a)) BY
               Auto)
   THEN (Assert d(a;c) < (d(b;c) + d(c;a)) BY
               Auto)
   THEN (RW  (AddrC [1] (LemmaC `real-vec-dist-symmetry`)) (-1) THENA Auto)
   THEN nRAdd ⌜-(d(c;a))⌝ (-1)⋅
   THEN RWO "real-vec-dist-same-zero" 0
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}a,b,c:Point.    (ba>ac  {}\mRightarrow{}  b  \#  c)


By

---

Latex:
(UnfoldGeoAbbreviations  0
  THEN  Auto
  THEN  (Assert  d(b;a)  \mleq{}  (d(b;c)  +  d(c;a))  BY
                          Auto)
  THEN  (Assert  d(a;c)  <  (d(b;c)  +  d(c;a))  BY
                          Auto)
  THEN  (RW    (AddrC  [1]  (LemmaC  `real-vec-dist-symmetry`))  (-1)  THENA  Auto)
  THEN  nRAdd  \mkleeneopen{}-(d(c;a))\mkleeneclose{}  (-1)\mcdot{}
  THEN  RWO  "real-vec-dist-same-zero"  0
  THEN  Auto)

---

Home Index