---

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


1. e : BasicGeometry
2. x : {p:Point| B(OXp)} 
3. y : {p:Point| B(OXp)} 
4. z : {p:Point| B(OXp)} 
⊢ extend Oz by Xx ≡ extend Oz by Xy ⇒ x ≡ y
BY
{ GeneralizeGeoExtends [`a';`b'] }

1
1. e : BasicGeometry
2. x : {p:Point| B(OXp)} 
3. y : {p:Point| B(OXp)} 
4. z : {p:Point| B(OXp)} 
5. a : {x1:Point| B(Ozx1) ∧ zx1 ≅ Xx} 
6. za ≅ Xx ∧ B(Oza)
7. b : {x:Point| B(Ozx) ∧ zx ≅ Xy} 
8. zb ≅ Xy ∧ B(Ozb)
⊢ a ≡ b ⇒ x ≡ y

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  \{p:Point|  B(OXp)\} 
3.  y  :  \{p:Point|  B(OXp)\} 
4.  z  :  \{p:Point|  B(OXp)\} 
\mvdash{}  extend  Oz  by  Xx  \mequiv{}  extend  Oz  by  Xy  {}\mRightarrow{}  x  \mequiv{}  y


By

---

Latex:
GeneralizeGeoExtends  [`a';`b']

---

Home Index