---

Step * of Lemma Euclid-Prop2-lemma-ext

∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀v:Point.  (∃x:Point [ax ≅ bv])
BY
{ Extract of Obid: Euclid-Prop2-lemma
  not unfolding  geo-CCL geo-SCO geo-SCS
  finishing with (RepUR ``let prop2-lemma eqtri`` 0 THEN Auto)
  normalizes to:
  
  λe,A,B,C. lemma2(A;B;C) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \mneq{}  b\}  .  \mforall{}v:Point.    (\mexists{}x:Point  [ax  \mcong{}  bv])


By

---

Latex:
Extract  of  Obid:  Euclid-Prop2-lemma
not  unfolding    geo-CCL  geo-SCO  geo-SCS
finishing  with  (RepUR  ``let  prop2-lemma  eqtri``  0  THEN  Auto)
normalizes  to:

\mlambda{}e,A,B,C.  lemma2(A;B;C)

---

Home Index