---

Step * 1 of Lemma eu-add-length-cancel-left


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 = z ∈ Point)
10. a : Point@i
11. O_z_a ∧ za=Xx@i
12. b : Point@i
13. O_z_b ∧ zb=Xy@i
⊢ (a = b ∈ {p:Point| O_X_p} ) ⇒ (x = y ∈ {p:Point| O_X_p} )
BY
{ ((D 0 THENA Auto) THEN DSetVars THEN InstLemma `eu-construction-unicity` [⌜e⌝;⌜O⌝;⌜X⌝;⌜x⌝;⌜y⌝]⋅ 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  =  z)
10.  a  :  Point@i
11.  O\_z\_a  \mwedge{}  za=Xx@i
12.  b  :  Point@i
13.  O\_z\_b  \mwedge{}  zb=Xy@i
\mvdash{}  (a  =  b)  {}\mRightarrow{}  (x  =  y)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  DSetVars
  THEN  InstLemma  `eu-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}O\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index