---

Step * 1 2 of Lemma symmetric-point-construction1


1. e : BasicGeometry
2. a : Point
3. p : Point
4. [%1] : a # p
5. x : Point
6. B(pax) ∧ ax ≅ ap
⊢ ∃p':Point [p=a=p']
BY
{ ((D 0 With ⌜x⌝  THEN Auto) THEN D 0 THEN Auto) }

1
1. e : BasicGeometry
2. a : Point
3. p : Point
4. a # p
5. x : Point
6. B(pax)
7. ax ≅ ap
⊢ pa ≅ ax

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  Point
4.  [\%1]  :  a  \#  p
5.  x  :  Point
6.  B(pax)  \mwedge{}  ax  \mcong{}  ap
\mvdash{}  \mexists{}p':Point  [p=a=p']


By

---

Latex:
((D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)  THEN  D  0  THEN  Auto)

---

Home Index