---

Step * 5 1 1 2 of Lemma eu-eq_dist-axiomsA


1. g : EuclideanPlane
2. D' : Point
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. e : Point
8. f : Point
9. a' : Point
10. b' : Point
11. c' : Point
12. u : {u:Point| c' # u} 
13. B(a'b'c')
14. B(a'uc')
15. ab ≅ a'b'
16. cd ≅ b'c'
17. ef ≅ a'u
18. X' : Point
19. X-D'-X'
20. D'X' ≅ D'X
21. B(X'D'D')
22. D'D' ≅ cd
23. A : Point
24. B(XD'A)
25. D'A ≅ ab
26. O ≡ D'
⊢ B(AD'D')
BY
{ Auto }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  D'  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  d  :  Point
7.  e  :  Point
8.  f  :  Point
9.  a'  :  Point
10.  b'  :  Point
11.  c'  :  Point
12.  u  :  \{u:Point|  c'  \#  u\} 
13.  B(a'b'c')
14.  B(a'uc')
15.  ab  \mcong{}  a'b'
16.  cd  \mcong{}  b'c'
17.  ef  \mcong{}  a'u
18.  X'  :  Point
19.  X-D'-X'
20.  D'X'  \mcong{}  D'X
21.  B(X'D'D')
22.  D'D'  \mcong{}  cd
23.  A  :  Point
24.  B(XD'A)
25.  D'A  \mcong{}  ab
26.  O  \mequiv{}  D'
\mvdash{}  B(AD'D')


By

---

Latex:
Auto

---

Home Index