---

Step * of Lemma symmetric-point-unicity

∀e:BasicGeometry. ∀a,p,p1,p2:Point.  (p=a=p1 ⇒ p=a=p2 ⇒ p1 ≡ p2)
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. p : Point
4. p1 : Point
5. p2 : Point
6. p=a=p1
7. p=a=p2
⊢ p1 ≡ p2

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,p,p1,p2:Point.    (p=a=p1  {}\mRightarrow{}  p=a=p2  {}\mRightarrow{}  p1  \mequiv{}  p2)


By

---

Latex:
Auto

---

Home Index