---

Step * of Lemma eu-between-eq-seg-eq

∀e:EuclideanPlane. ∀a,b,c,a',b',c':Point.  (a_b_c ⇒ a'_b'_c' ⇒ ab=a'b' ⇒ ac=a'c' ⇒ bc=b'c')
BY
{ Auto }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. a' : Point@i
6. b' : Point@i
7. c' : Point@i
8. a_b_c@i
9. a'_b'_c'@i
10. ab=a'b'@i
11. ac=a'c'@i
⊢ bc=b'c'

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,a',b',c':Point.    (a\_b\_c  {}\mRightarrow{}  a'\_b'\_c'  {}\mRightarrow{}  ab=a'b'  {}\mRightarrow{}  ac=a'c'  {}\mRightarrow{}  bc=b'c')


By

---

Latex:
Auto

---

Home Index