---

Step * 1 1 1 1 1 of Lemma eu-conga-to-cong3


1. E : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. ¬(a = b ∈ Point)
9. ¬(c = b ∈ Point)
10. ¬(d = e ∈ Point)
11. ¬(f = e ∈ Point)
12. a' : Point
13. c' : Point
14. d' : Point
15. f' : Point
16. b_a_a'
17. b_c_c'
18. e_d_d'
19. e_f_f'
20. ba'=ed'
21. bc'=ef'
22. a'c'=d'f'
23. out(b a'a)
24. out(b cc')
25. out(e d'd)
26. out(e ff')
⊢ a'b=d'e ∧ bc'=ef' ∧ c'a'=f'd'
BY
{ Auto }

---

Latex:

---

Latex:

1.  E  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  \mneg{}(a  =  b)
9.  \mneg{}(c  =  b)
10.  \mneg{}(d  =  e)
11.  \mneg{}(f  =  e)
12.  a'  :  Point
13.  c'  :  Point
14.  d'  :  Point
15.  f'  :  Point
16.  b\_a\_a'
17.  b\_c\_c'
18.  e\_d\_d'
19.  e\_f\_f'
20.  ba'=ed'
21.  bc'=ef'
22.  a'c'=d'f'
23.  out(b  a'a)
24.  out(b  cc')
25.  out(e  d'd)
26.  out(e  ff')
\mvdash{}  a'b=d'e  \mwedge{}  bc'=ef'  \mwedge{}  c'a'=f'd'


By

---

Latex:
Auto

---

Home Index