---

Step * of Lemma Euclid-Prop9-ext

No Annotations
∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| c # ba} .  ∃f:Point. acf ≅a bcf
BY
{ Extract of Obid: Euclid-Prop9
  not unfolding  midpoint-construction geo-extend geo-M
  finishing with (RepUR ``let`` 0 THEN Auto)
  normalizes to:
  
  λe,a,b,c. <Mid(extend ca by cb;extend cb by ca)
            , <<<e "Ssquashstable" a c a a Ax, e "Ssquashstable" c Mid(extend ca by cb;extend cb by ca) c c Ax>
               , e "Ssquashstable" b c b b Ax
               >
              , e "Ssquashstable" c Mid(extend ca by cb;extend cb by ca) c c Ax
              >
            , extend ca by cb
            , Mid(extend ca by cb;extend cb by ca)
            , extend cb by ca
            , Mid(extend ca by cb;extend cb by ca)
            , <<λv.Ax, λv.Ax>, λv.Ax>
            , <<λv.Ax, λv.Ax>, λv.Ax>
            , <<λv.Ax, λv.Ax>, λv.Ax>
            , <<λv.Ax, λv.Ax>, λv.Ax>
            , λv.Ax
            , λv.Ax
            , λv.Ax> }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  c  \#  ba\}  .    \mexists{}f:Point.  acf  \mcong{}\msuba{}  bcf


By

---

Latex:
Extract  of  Obid:  Euclid-Prop9
not  unfolding    midpoint-construction  geo-extend  geo-M
finishing  with  (RepUR  ``let``  0  THEN  Auto)
normalizes  to:

\mlambda{}e,a,b,c.  <Mid(extend  ca  by  cb;extend  cb  by  ca)
                    ,  <<<e  "Ssquashstable"  a  c  a  a  Ax
                            ,  e  "Ssquashstable"  c  Mid(extend  ca  by  cb;extend  cb  by  ca)  c  c  Ax
                            >
                          ,  e  "Ssquashstable"  b  c  b  b  Ax
                          >
                        ,  e  "Ssquashstable"  c  Mid(extend  ca  by  cb;extend  cb  by  ca)  c  c  Ax
                        >
                    ,  extend  ca  by  cb
                    ,  Mid(extend  ca  by  cb;extend  cb  by  ca)
                    ,  extend  cb  by  ca
                    ,  Mid(extend  ca  by  cb;extend  cb  by  ca)
                    ,  <<\mlambda{}v.Ax,  \mlambda{}v.Ax>,  \mlambda{}v.Ax>
                    ,  <<\mlambda{}v.Ax,  \mlambda{}v.Ax>,  \mlambda{}v.Ax>
                    ,  <<\mlambda{}v.Ax,  \mlambda{}v.Ax>,  \mlambda{}v.Ax>
                    ,  <<\mlambda{}v.Ax,  \mlambda{}v.Ax>,  \mlambda{}v.Ax>
                    ,  \mlambda{}v.Ax
                    ,  \mlambda{}v.Ax
                    ,  \mlambda{}v.Ax>

---

Home Index