---

Step * 2 1 1 1 1 of Lemma geo-zero-length-iff


1. e : BasicGeometry
2. a : Point
3. b : Point
4. z : {x:Point| O_X_x ∧ Xx ≅ ab} 
5. a ≡ b
6. {Xz ≅ bb}
7. O_z_z
8. X ≡ z
⊢ z ≡ X
BY
{ Auto }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  z  :  \{x:Point|  O\_X\_x  \mwedge{}  Xx  \00D0  ab\} 
5.  a  \mequiv{}  b
6.  \{Xz  \00D0  bb\}
7.  O\_z\_z
8.  X  \mequiv{}  z
\mvdash{}  z  \mequiv{}  X


By

---

Latex:
Auto

---

Home Index