---

Step * 1 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. 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'
BY
{ Auto }

---

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.  ab=a'b'  \mwedge{}  bc=b'c'  \mwedge{}  ca=c'a'@i
12.  ad=a'd'@i
13.  bd=b'd'@i
14.  \mneg{}(a  =  b)@i
\mvdash{}  ac=a'c'


By

---

Latex:
Auto

---

Home Index