---

Step * of Lemma symmetric-point-construction

∀e:BasicGeometry. ∀a,p:Point.  (a ≠ p ⇒ (∃p':Point. p=a=p'))
BY
{ (Auto THEN D 0 With ⌜SymmetricPoint(a;p)⌝  THEN Auto) }

1
1. e : BasicGeometry
2. a : Point
3. p : Point
4. a ≠ p
⊢ p=a=SymmetricPoint(a;p)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,p:Point.    (a  \mneq{}  p  {}\mRightarrow{}  (\mexists{}p':Point.  p=a=p'))


By

---

Latex:
(Auto  THEN  D  0  With  \mkleeneopen{}SymmetricPoint(a;p)\mkleeneclose{}    THEN  Auto)

---

Home Index