---

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


∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab)
BY
{ (UnfoldGeoAbbreviations 0 THEN (RWO "rv-congruent-iff2< real-vec-sep-iff2< r2-be-iff<" 0 THENA Auto)) }

1
∀a,b,c:ℝ^2.  (a_b_c ⇒ b ≠ c ⇒ (d(a;b) < d(a;c)))

---

Latex:

---

Latex:

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


By

---

Latex:
(UnfoldGeoAbbreviations  0
  THEN  (RWO  "rv-congruent-iff2<  real-vec-sep-iff2<  r2-be-iff<"  0  THENA  Auto)
  )

---

Home Index