---

Step * 1 of Lemma symmetric-point-construction


1. e : BasicGeometry
2. a : Point
3. p : Point
4. a ≠ p
⊢ p=a=SymmetricPoint(a;p)
BY
{ (GenConclTerm ⌜SymmetricPoint(a;p)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  Point
4.  a  \mneq{}  p
\mvdash{}  p=a=SymmetricPoint(a;p)


By

---

Latex:
(GenConclTerm  \mkleeneopen{}SymmetricPoint(a;p)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index