---

Step * 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. bac = BAC@i
⊢ bc=BC
BY
{ D -1 }

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))
∧ (¬(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

---

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.  bac  =  BAC@i
\mvdash{}  bc=BC


By

---

Latex:
D  -1

---

Home Index