---

Step * of Lemma Euclid-midpoint-1

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} .  (∃d:Point [a=d=b])
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
⊢ ∃d:Point [a=d=b]

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .    (\mexists{}d:Point  [a=d=b])


By

---

Latex:
Auto

---

Home Index