---

Step * of Lemma Euclid-Prop2-ext

No Annotations
∀e:EuclideanPlane. ∀a,b,c:Point.  (∃x:Point [ax ≅ bc])
BY
{ Extract of Obid: Euclid-Prop2
  not unfolding  prop2-lemma geo-O geo-X geo-M
  finishing with Auto
  normalizes to:
  
  λe,a,b,c. if M(O;X;a) then if M(a;O;b) then lemma2(a;b;c) else lemma2(a;O;lemma2(O;b;c)) fi 
           if M(a;X;b) then lemma2(a;b;c)
           else lemma2(a;X;lemma2(X;b;c))
           fi  }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (\mexists{}x:Point  [ax  \mcong{}  bc])


By

---

Latex:
Extract  of  Obid:  Euclid-Prop2
not  unfolding    prop2-lemma  geo-O  geo-X  geo-M
finishing  with  Auto
normalizes  to:

\mlambda{}e,a,b,c.  if  M(O;X;a)  then  if  M(a;O;b)  then  lemma2(a;b;c)  else  lemma2(a;O;lemma2(O;b;c))  fi 
                  if  M(a;X;b)  then  lemma2(a;b;c)
                  else  lemma2(a;X;lemma2(X;b;c))
                  fi 

---

Home Index