---

Step * 1 of Lemma symmetric-point-construction1


1. e : BasicGeometry
2. a : Point
3. p : {p:Point| a # p} 
⊢ ∃p':Point [p=a=p']
BY
{ (D -1 THEN (gProlong ⌜p⌝ ⌜a⌝ `x' ⌜a⌝ ⌜p⌝ ⋅ THENA Auto)) }

1
.....antecedent..... 
1. e : BasicGeometry
2. a : Point
3. p : Point
4. [%1] : a # p
⊢ p # a

2
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']

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  \{p:Point|  a  \#  p\} 
\mvdash{}  \mexists{}p':Point  [p=a=p']


By

---

Latex:
(D  -1  THEN  (gProlong  \mkleeneopen{}p\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}  `x'  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}p\mkleeneclose{}  \mcdot{}  THENA  Auto))

---

Home Index