---

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


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

1
∀a,b,c,d:ℝ^2.  (a_b_d ⇒ b_c_d ⇒ a_b_c)

---

Latex:

---

Latex:

\mforall{}a,b,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc))


By

---

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

---

Home Index