---

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


∀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)
BY
{ (InstLemma `rv-be-five-segment` []⋅ THENM Trivial) }

---

Latex:

---

Latex:

\mforall{}a,b,c,d,A,B,C,D:\mBbbR{}\^{}2.    (a  \mneq{}  b  {}\mRightarrow{}  a\_b\_c  {}\mRightarrow{}  A\_B\_C  {}\mRightarrow{}  ab=AB  {}\mRightarrow{}  bc=BC  {}\mRightarrow{}  ad=AD  {}\mRightarrow{}  bd=BD  {}\mRightarrow{}  cd=CD)


By

---

Latex:
(InstLemma  `rv-be-five-segment`  []\mcdot{}  THENM  Trivial)

---

Home Index