---

Step * of Lemma euclid-P3-ext

∀e:EuclideanPlane. ∀A,B,C1,C2:Point.  ∃E:Point. (A_E_B ∧ AE=C1C2) supposing (¬(C1 = C2 ∈ Point)) ∧ |C1C2| < |AB|
BY
{ Extract of Obid: euclid-P3
  normalizes to:
  
  λe,A,B,C1,C2. <e "extend" (e "extend" B A C1 C2) A C1 C2, let %2,%3 = e "Tdef" in %3 (λ%.Ax), e "Estable">
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C1,C2:Point.
    \mexists{}E:Point.  (A\_E\_B  \mwedge{}  AE=C1C2)  supposing  (\mneg{}(C1  =  C2))  \mwedge{}  |C1C2|  <  |AB|


By

---

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

\mlambda{}e,A,B,C1,C2.  <e  "extend"  (e  "extend"  B  A  C1  C2)  A  C1  C2
                            ,  let  \%2,\%3  =  e  "Tdef" 
                                in  \%3  (\mlambda{}\%.Ax)
                            ,  e  "Estable">
finishing  with  Auto

---

Home Index