---

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


1. e : BasicGeometry
2. a : Point
3. b : Point
4. a ≡ b
5. z : {x:Point| O_X_x ∧ Xx ≅ ab} 
6. Xz ≅ ab
7. O_X_z
⊢ z ≡ X
BY
{ (gEliminatePoint' 4 THENA Auto) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
(gEliminatePoint'  4  THENA  Auto)

---

Home Index