---

Step * 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))
∧ (¬(B = A ∈ Point))
∧ (¬(C = A ∈ Point))
∧ (∃a',c',x',z':Point. (a_b_a' ∧ a_c_c' ∧ A_B_x' ∧ A_C_z' ∧ aa'=Ax' ∧ ac'=Az' ∧ a'c'=x'z'))@i
⊢ bc=BC
BY
{ ExRepD }

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. 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

---

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))
\mwedge{}  (\mneg{}(B  =  A))
\mwedge{}  (\mneg{}(C  =  A))
\mwedge{}  (\mexists{}a',c',x',z':Point.  (a\_b\_a'  \mwedge{}  a\_c\_c'  \mwedge{}  A\_B\_x'  \mwedge{}  A\_C\_z'  \mwedge{}  aa'=Ax'  \mwedge{}  ac'=Az'  \mwedge{}  a'c'=x'z'))@i
\mvdash{}  bc=BC


By

---

Latex:
ExRepD

---

Home Index