---

Step * 1 1 1 of Lemma eu-sas


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. Triangle(a;b;c)
9. Triangle(A;B;C)
10. ab=AB@i
11. ac=AC@i
12. ¬(b = a ∈ Point)@i
13. ¬(c = a ∈ Point)@i
14. ¬(B = A ∈ Point)@i
15. ¬(C = A ∈ Point)@i
16. a' : Point@i
17. c' : Point@i
18. x' : Point@i
19. z' : Point@i
20. a_b_a'@i
21. a_c_c'@i
22. A_B_x'@i
23. A_C_z'@i
24. aa'=Ax'@i
25. ac'=Az'@i
26. a'c'=x'z'@i
⊢ bc=BC
BY
{ (AddSegmentCongruences THEN Auto) }

---

Latex:

---

Latex:

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.  Triangle(a;b;c)
9.  Triangle(A;B;C)
10.  ab=AB@i
11.  ac=AC@i
12.  \mneg{}(b  =  a)@i
13.  \mneg{}(c  =  a)@i
14.  \mneg{}(B  =  A)@i
15.  \mneg{}(C  =  A)@i
16.  a'  :  Point@i
17.  c'  :  Point@i
18.  x'  :  Point@i
19.  z'  :  Point@i
20.  a\_b\_a'@i
21.  a\_c\_c'@i
22.  A\_B\_x'@i
23.  A\_C\_z'@i
24.  aa'=Ax'@i
25.  ac'=Az'@i
26.  a'c'=x'z'@i
\mvdash{}  bc=BC


By

---

Latex:
(AddSegmentCongruences  THEN  Auto)

---

Home Index