---

Step * of Lemma symmetric-point-construction1

No Annotations
∀e:BasicGeometry. ∀a:Point. ∀p:{p:Point| a # p} .  (∃p':Point [p=a=p'])
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. p : {p:Point| a # p} 
⊢ ∃p':Point [p=a=p']

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a:Point.  \mforall{}p:\{p:Point|  a  \#  p\}  .    (\mexists{}p':Point  [p=a=p'])


By

---

Latex:
Auto

---

Home Index