---

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


∀a,b,c:ℝ^2.  (a_b_c ⇒ b ≠ c ⇒ (d(a;b) < d(a;c)))
BY
{ ((Auto THEN (FLemma `rv-be-dist` [-2] THENA Auto)) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

\mforall{}a,b,c:\mBbbR{}\^{}2.    (a\_b\_c  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  (d(a;b)  <  d(a;c)))


By

---

Latex:
((Auto  THEN  (FLemma  `rv-be-dist`  [-2]  THENA  Auto))  THEN  RWO  "-1"  0  THEN  Auto)

---

Home Index