---

Step * 1 1 1 1 of Lemma eu-add-length-assoc

.....assertion..... 
1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. y : Point
5. O_X_y
6. z : Point
7. O_X_z
8. ¬(O = X ∈ Point)
9. ¬(O = x ∈ Point)
10. ¬(O = y ∈ Point)
11. a : Point@i
12. O_y_a ∧ ya=Xz@i
13. b : Point@i
14. O_x_b ∧ xb=Xa@i
15. c : Point@i
16. O_x_c ∧ xc=Xy@i
17. ¬(O = c ∈ Point)
18. d : Point@i
19. O_c_d ∧ cd=Xz@i
⊢ (|Xa| = |Xy| + |ya| ∈ {p:Point| O_X_p} ) ∧ (|xd| = |xc| + |cd| ∈ {p:Point| O_X_p} )
BY
{ (D 0 THEN BLemma `eu-add-length-between` THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanPlane
2.  x  :  Point
3.  O\_X\_x
4.  y  :  Point
5.  O\_X\_y
6.  z  :  Point
7.  O\_X\_z
8.  \mneg{}(O  =  X)
9.  \mneg{}(O  =  x)
10.  \mneg{}(O  =  y)
11.  a  :  Point@i
12.  O\_y\_a  \mwedge{}  ya=Xz@i
13.  b  :  Point@i
14.  O\_x\_b  \mwedge{}  xb=Xa@i
15.  c  :  Point@i
16.  O\_x\_c  \mwedge{}  xc=Xy@i
17.  \mneg{}(O  =  c)
18.  d  :  Point@i
19.  O\_c\_d  \mwedge{}  cd=Xz@i
\mvdash{}  (|Xa|  =  |Xy|  +  |ya|)  \mwedge{}  (|xd|  =  |xc|  +  |cd|)


By

---

Latex:
(D  0  THEN  BLemma  `eu-add-length-between`  THEN  Auto)

---

Home Index