---

Step * 1 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
10. p ≠ a
⊢ p1 ≡ p2
BY
{ (InstLemma `geo-construction-unicity` [⌜e⌝;⌜p⌝;⌜a⌝;⌜p1⌝;⌜p2⌝]⋅ THEN Auto) }

---

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
10.  p  \mneq{}  a
\mvdash{}  p1  \mequiv{}  p2


By

---

Latex:
(InstLemma  `geo-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index