---

Step * 1 of Lemma eu-5segSAS


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. f : Point
6. g : Point
7. A : Point
8. B : Point
9. C : Point
10. F : Point
11. G : Point
12. Triangle(a;f;g)
13. Triangle(A;F;G)
14. a_f_b
15. a_g_c
16. A_F_B
17. A_G_C
18. af=AF
19. fb=FB
20. bc=BC
21. ag=AG
22. gc=GC
⊢ fg=FG
BY
{ (AddSegmentCongruences⋅ THENA Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. f : Point
6. g : Point
7. A : Point
8. B : Point
9. C : Point
10. F : Point
11. G : Point
12. Triangle(a;f;g)
13. Triangle(A;F;G)
14. a_f_b
15. a_g_c
16. A_F_B
17. A_G_C
18. af=AF
19. fb=FB
20. bc=BC
21. ag=AG
22. gc=GC
23. ac=AC
24. ca=CA
25. ab=AB
26. ba=BA
27. fc=FC
28. GB=gb
29. GF=gf
⊢ fg=FG

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  f  :  Point
6.  g  :  Point
7.  A  :  Point
8.  B  :  Point
9.  C  :  Point
10.  F  :  Point
11.  G  :  Point
12.  Triangle(a;f;g)
13.  Triangle(A;F;G)
14.  a\_f\_b
15.  a\_g\_c
16.  A\_F\_B
17.  A\_G\_C
18.  af=AF
19.  fb=FB
20.  bc=BC
21.  ag=AG
22.  gc=GC
\mvdash{}  fg=FG


By

---

Latex:
(AddSegmentCongruences\mcdot{}  THENA  Auto)

---

Home Index