---

Step * of Lemma euclid-P1-ext

∀e:EuclideanPlane. ∀A,B:Point.  ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A = B ∈ Point)
BY
{ Extract of Obid: euclid-P1
  normalizes to:
  
  λe,A,B. let z1,z2,_,h,_,_,_ = TERMOF{circle-circle-continuity:o, \\v:l, i:l} e A B B A A (e "extend" A B A B) A 
                                (e "extend" A B A B) in 
          <z2, h, e "Estable", e "Estable">
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B:Point.    \mexists{}C:Point.  (AC=AB  \mwedge{}  BC=AB  \mwedge{}  AC=BC)  supposing  \mneg{}(A  =  B)


By

---

Latex:
Extract  of  Obid:  euclid-P1
normalizes  to:

\mlambda{}e,A,B.  let  z1,z2,$_{}$,h,$_{}$,$_{}$,\mbackslash{}f\000Cf24_{}$  =  TERMOF\{circle-circle-continuity:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  e  A  B  B  A  A 
                                                    (e  "extend"  A  B  A  B) 
                                                    A 
                                                    (e  "extend"  A  B  A  B)  in 
                <z2,  h,  e  "Estable",  e  "Estable">
finishing  with  Auto

---

Home Index