---

Step * 1 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
9. pa ≅ ap2
⊢ p1 ≡ p2
BY
{ (gSeparatedCases' ⌜p⌝ ⌜a⌝⋅ THENA Auto) }

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
10. p ≠ a
⊢ 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
9.  pa  \00D0  ap2
\mvdash{}  p1  \mequiv{}  p2


By

---

Latex:
(gSeparatedCases'  \mkleeneopen{}p\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index