---

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


1. g : EuclideanPlane
2. A : 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-A-X'
20. AX' ≅ AX
21. D' : Point
22. B(X'AD')
23. AD' ≅ cd
24. B(XAA)
25. AA ≅ ab
26. A # D'
27. O ≡ A
⊢ B(AAD')
BY
{ Auto }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  A  :  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-A-X'
20.  AX'  \mcong{}  AX
21.  D'  :  Point
22.  B(X'AD')
23.  AD'  \mcong{}  cd
24.  B(XAA)
25.  AA  \mcong{}  ab
26.  A  \#  D'
27.  O  \mequiv{}  A
\mvdash{}  B(AAD')


By

---

Latex:
Auto

---

Home Index