---

Step * of Lemma symmetric-point-unicity2

∀e:BasicGeometry. ∀a,p,p1,p2:Point.  (p1=a=p ⇒ p2=a=p ⇒ p1 ≡ p2)
BY
{ (Auto THEN UsingVars [`a';`p'] (BLemma `symmetric-point-unicity`) THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  UsingVars  [`a';`p']  (BLemma  `symmetric-point-unicity`)  THEN  EAuto  1)

---

Home Index