---

Step * of Lemma Euclid-midpoint

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} .  (∃d:{Point| a=d=b})
BY
{ ((UnivCD THENA Auto) THEN UseWitness ⌜Mid(a;b)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .    (\mexists{}d:\{Point|  a=d=b\})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  UseWitness  \mkleeneopen{}Mid(a;b)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index