---

Step * of Lemma Euclid-Prop10-ext

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} .  (∃d:Point [(a-d-b ∧ ad ≅ db)])
BY
{ Extract of Obid: Euclid-Prop10
  not unfolding  midpoint-construction
  finishing with Auto
  normalizes to:
  
  λe,a,b. Mid(a;b) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .    (\mexists{}d:Point  [(a-d-b  \mwedge{}  ad  \mcong{}  db)])


By

---

Latex:
Extract  of  Obid:  Euclid-Prop10
not  unfolding    midpoint-construction
finishing  with  Auto
normalizes  to:

\mlambda{}e,a,b.  Mid(a;b)

---

Home Index