---

Step * 1 of Lemma eu-three-segment


1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [A] : Point
6. [B] : Point
7. [C] : Point
8. ¬(a = b ∈ Point)
9. [%] : a_b_c
10. [%4] : A_B_C
11. [%6] : ab=AB
12. [%8] : bc=BC
13. (ca=CA) supposing (ba=BA and aa=AA)
⊢ ac=AC
BY
{ (D -1 THENA Auto) }

1
1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [A] : Point
6. [B] : Point
7. [C] : Point
8. ¬(a = b ∈ Point)
9. [%] : a_b_c
10. [%4] : A_B_C
11. [%6] : ab=AB
12. [%8] : bc=BC
13. ca=CA supposing ba=BA
⊢ ac=AC

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  [a]  :  Point
3.  [b]  :  Point
4.  [c]  :  Point
5.  [A]  :  Point
6.  [B]  :  Point
7.  [C]  :  Point
8.  \mneg{}(a  =  b)
9.  [\%]  :  a\_b\_c
10.  [\%4]  :  A\_B\_C
11.  [\%6]  :  ab=AB
12.  [\%8]  :  bc=BC
13.  (ca=CA)  supposing  (ba=BA  and  aa=AA)
\mvdash{}  ac=AC


By

---

Latex:
(D  -1  THENA  Auto)

---

Home Index