---

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


∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)
BY
{ (UnfoldGeoAbbreviations 0 THEN (RWO "rv-congruent-iff2< real-vec-sep-iff2< r2-be-iff<" 0 THENA Auto)) }

1
∀a,b,c,d,A,B,C,D:ℝ^2.  (a ≠ b ⇒ a_b_c ⇒ A_B_C ⇒ ab=AB ⇒ bc=BC ⇒ ad=AD ⇒ bd=BD ⇒ cd=CD)

---

Latex:

---

Latex:

\mforall{}a,b,c,d,A,B,C,D:Point.
    (a  \#  b  {}\mRightarrow{}  B(abc)  {}\mRightarrow{}  B(ABC)  {}\mRightarrow{}  ab  \mcong{}  AB  {}\mRightarrow{}  bc  \mcong{}  BC  {}\mRightarrow{}  ad  \mcong{}  AD  {}\mRightarrow{}  bd  \mcong{}  BD  {}\mRightarrow{}  cd  \mcong{}  CD)


By

---

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

---

Home Index