---

Step * 1 1 1 of Lemma eu-fsc-ap


1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. d : Point@i
6. a' : Point@i
7. b' : Point@i
8. c' : Point@i
9. d' : Point@i
10. Colinear(a;b;c)@i
11. Cong3(abc,a'b'c')@i
12. ad=a'd'@i
13. bd=b'd'@i
14. ¬(a = b ∈ Point)@i
⊢ ac=a'c'
BY
{ Unfold `eu-cong-tri` 11 }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. d : Point@i
6. a' : Point@i
7. b' : Point@i
8. c' : Point@i
9. d' : Point@i
10. Colinear(a;b;c)@i
11. ab=a'b' ∧ bc=b'c' ∧ ca=c'a'@i
12. ad=a'd'@i
13. bd=b'd'@i
14. ¬(a = b ∈ Point)@i
⊢ ac=a'c'

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  a  :  Point@i
3.  b  :  Point@i
4.  c  :  Point@i
5.  d  :  Point@i
6.  a'  :  Point@i
7.  b'  :  Point@i
8.  c'  :  Point@i
9.  d'  :  Point@i
10.  Colinear(a;b;c)@i
11.  Cong3(abc,a'b'c')@i
12.  ad=a'd'@i
13.  bd=b'd'@i
14.  \mneg{}(a  =  b)@i
\mvdash{}  ac=a'c'


By

---

Latex:
Unfold  `eu-cong-tri`  11

---

Home Index