---

Step * 1 1 1 1 1 1 1 of Lemma eu-between-eq-same-side

.....assertion..... 
1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. A_B_D
7. A_B_C
8. ¬(A = B ∈ Point)
9. ¬A_C_D
10. ¬A_D_C
11. ¬(A = D ∈ Point)
12. C' : Point
13. A_D_C'
14. DC'=CD
15. ¬(A = C ∈ Point)
16. D' : Point
17. A_C_D'
18. CD'=CD
19. ¬(A = C' ∈ Point)
20. B' : Point
21. A_C'_B'
22. C'B'=CB
23. ¬(A = D' ∈ Point)
24. B'' : Point
25. A_D'_B''
26. D'B''=DB
27. ¬(B = C ∈ Point)
28. ¬(B = D ∈ Point)
29. ¬(B'' = D' ∈ Point)
30. BC'=B''C
31. B_D'_B''
32. B_C'_B'
33. |BD'| = |BC| + |CD'| ∈ {p:Point| O_X_p} 
34. |BC'| = |BD| + |DC'| ∈ {p:Point| O_X_p} 
35. |BB''| = |BD'| + |D'B''| ∈ {p:Point| O_X_p} 
36. |BB'| = |BC'| + |C'B'| ∈ {p:Point| O_X_p} 
⊢ |BC| + |CD'| + |D'B''| = |D'B''| + |CD'| + |BC| ∈ {p:Point| O_X_p} 
BY
{ (GenConclTerms Auto [⌜|BC|⌝;⌜|CD'|⌝;⌜|D'B''|⌝]⋅ THEN All Thin) }

1
1. e : EuclideanPlane
2. v : {p:Point| O_X_p} 
3. v1 : {p:Point| O_X_p} 
4. v2 : {p:Point| O_X_p} 
⊢ v + v1 + v2 = v2 + v1 + v ∈ {p:Point| O_X_p} 

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanPlane
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  D  :  Point
6.  A\_B\_D
7.  A\_B\_C
8.  \mneg{}(A  =  B)
9.  \mneg{}A\_C\_D
10.  \mneg{}A\_D\_C
11.  \mneg{}(A  =  D)
12.  C'  :  Point
13.  A\_D\_C'
14.  DC'=CD
15.  \mneg{}(A  =  C)
16.  D'  :  Point
17.  A\_C\_D'
18.  CD'=CD
19.  \mneg{}(A  =  C')
20.  B'  :  Point
21.  A\_C'\_B'
22.  C'B'=CB
23.  \mneg{}(A  =  D')
24.  B''  :  Point
25.  A\_D'\_B''
26.  D'B''=DB
27.  \mneg{}(B  =  C)
28.  \mneg{}(B  =  D)
29.  \mneg{}(B''  =  D')
30.  BC'=B''C
31.  B\_D'\_B''
32.  B\_C'\_B'
33.  |BD'|  =  |BC|  +  |CD'|
34.  |BC'|  =  |BD|  +  |DC'|
35.  |BB''|  =  |BD'|  +  |D'B''|
36.  |BB'|  =  |BC'|  +  |C'B'|
\mvdash{}  |BC|  +  |CD'|  +  |D'B''|  =  |D'B''|  +  |CD'|  +  |BC|


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}|BC|\mkleeneclose{};\mkleeneopen{}|CD'|\mkleeneclose{};\mkleeneopen{}|D'B''|\mkleeneclose{}]\mcdot{}  THEN  All  Thin)

---

Home Index