---

Step * 1 1 of Lemma symmetric-point-unicity


1. e : BasicGeometry
2. a : Point
3. p : Point
4. p1 : Point
5. p2 : Point
6. p_a_p1
7. pa ≅ ap1
8. p=a=p2
⊢ p1 ≡ p2
BY
{ D -1 }

1
1. e : BasicGeometry
2. a : Point
3. p : Point
4. p1 : Point
5. p2 : Point
6. p_a_p1
7. pa ≅ ap1
8. p_a_p2
9. pa ≅ ap2
⊢ p1 ≡ p2

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  Point
4.  p1  :  Point
5.  p2  :  Point
6.  p\_a\_p1
7.  pa  \00D0  ap1
8.  p=a=p2
\mvdash{}  p1  \mequiv{}  p2


By

---

Latex:
D  -1

---

Home Index