---

Step * 1 1 1 of Lemma geo-add-length-zero


1. e : BasicGeometry
2. x : {p:Point| O_X_p} 
3. a : {x1:Point| O_x_x1 ∧ xx1 ≅ XX} 
4. xa ≅ XX
5. O_x_a
⊢ a ≡ x
BY
{ (FLemma `geo-congruence-identity-sym` [-2] THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  \{p:Point|  O\_X\_p\} 
3.  a  :  \{x1:Point|  O\_x\_x1  \mwedge{}  xx1  \00D0  XX\} 
4.  xa  \00D0  XX
5.  O\_x\_a
\mvdash{}  a  \mequiv{}  x


By

---

Latex:
(FLemma  `geo-congruence-identity-sym`  [-2]  THEN  EAuto  1)

---

Home Index