---

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


1. g : EuclideanPlane
2. t : Point
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. e : Point
8. f : Point
9. x : Point
10. y : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. u : {u:Point| c' # u} 
15. B(tb'c')
16. B(tuc')
17. ab ≅ tb'
18. cd ≅ b'c'
19. ef ≅ tu
20. ¬D(x;y;y;y;e;f)
21. ¬xy > ef
22. ef ≥ xy
23. t # c'
24. B : Point
25. c'-t-B
26. tB ≅ c't
27. B(Btt)
28. tt ≅ xy
29. |a'c'| = |ef| + |uc'| ∈ Length
30. |a'u| = |ef| ∈ Length
31. |ef| ≤ |a'c'|
32. |a't| ≤ |a'c'|
33. |xy| = |a't| ∈ Length
34. a' ≡ t
⊢ B(ttc')
BY
{ Auto }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  t  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  d  :  Point
7.  e  :  Point
8.  f  :  Point
9.  x  :  Point
10.  y  :  Point
11.  a'  :  Point
12.  b'  :  Point
13.  c'  :  Point
14.  u  :  \{u:Point|  c'  \#  u\} 
15.  B(tb'c')
16.  B(tuc')
17.  ab  \mcong{}  tb'
18.  cd  \mcong{}  b'c'
19.  ef  \mcong{}  tu
20.  \mneg{}D(x;y;y;y;e;f)
21.  \mneg{}xy  >  ef
22.  ef  \mgeq{}  xy
23.  t  \#  c'
24.  B  :  Point
25.  c'-t-B
26.  tB  \mcong{}  c't
27.  B(Btt)
28.  tt  \mcong{}  xy
29.  |a'c'|  =  |ef|  +  |uc'|
30.  |a'u|  =  |ef|
31.  |ef|  \mleq{}  |a'c'|
32.  |a't|  \mleq{}  |a'c'|
33.  |xy|  =  |a't|
34.  a'  \mequiv{}  t
\mvdash{}  B(ttc')


By

---

Latex:
Auto

---

Home Index