---

Step * of Lemma geo-extend-construction-ext

∀e:EuclideanPlane. ∀q:Point. ∀a:{a:Point| q ≠ a} . ∀b,c:Point.  (∃x:{Point| (q_a_x ∧ ax ≅ bc)})
BY
{ Extract of Obid: geo-extend-construction
  normalizes to:
  
  λe,q,a,b,c. SCO(q;a;a;if M(O;X;a)
                          then if M(a;O;b) then prop2-lemma(e;a;b;c) else prop2-lemma(e;a;O;prop2-lemma(e;O;b;c)) fi 
             if M(a;X;b) then prop2-lemma(e;a;b;c)
             else prop2-lemma(e;a;X;prop2-lemma(e;X;b;c))
             fi )
  
  not unfolding  prop2-lemma geo-O geo-X geo-SCO geo-M
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}q:Point.  \mforall{}a:\{a:Point|  q  \mneq{}  a\}  .  \mforall{}b,c:Point.    (\mexists{}x:\{Point|  (q\_a\_x  \mwedge{}  ax  \00D0  bc)\})


By

---

Latex:
Extract  of  Obid:  geo-extend-construction
normalizes  to:

\mlambda{}e,q,a,b,c.  SCO(q;a;a;if  M(O;X;a)
                                                then  if  M(a;O;b)
                                                          then  prop2-lemma(e;a;b;c)
                                                          else  prop2-lemma(e;a;O;prop2-lemma(e;O;b;c))
                                                          fi 
                      if  M(a;X;b)  then  prop2-lemma(e;a;b;c)
                      else  prop2-lemma(e;a;X;prop2-lemma(e;X;b;c))
                      fi  )

not  unfolding    prop2-lemma  geo-O  geo-X  geo-SCO  geo-M
finishing  with  Auto

---

Home Index