---

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


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
20. xd=Xa
⊢ b = d ∈ Point
BY
{ (InstLemma `eu-construction-unicity` [⌜e⌝;⌜O⌝;⌜x⌝;⌜b⌝;⌜d⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

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
20.  xd=Xa
\mvdash{}  b  =  d


By

---

Latex:
(InstLemma  `eu-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index