---

Step * of Lemma Euclid-erect-perp-ext

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} . ∀c:{c:Point| Colinear(a;b;c)} .  (∃p:Point [(ab  ⊥c pc ∧ p # ab)])
BY
{ Extract of Obid: Euclid-erect-perp
  not unfolding  geo-M sympoint eqtri 
  finishing with Auto
  normalizes to:
  
  λe,a,b,c. if M(a;b;c) then Δ(a;SymmetricPoint(c;a)) else Δ(b;SymmetricPoint(c;b)) fi  }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c:\{c:Point|  Colinear(a;b;c)\}  .
    (\mexists{}p:Point  [(ab    \mbot{}c  pc  \mwedge{}  p  \#  ab)])


By

---

Latex:
Extract  of  Obid:  Euclid-erect-perp
not  unfolding    geo-M  sympoint  eqtri 
finishing  with  Auto
normalizes  to:

\mlambda{}e,a,b,c.  if  M(a;b;c)  then  \mDelta{}(a;SymmetricPoint(c;a))  else  \mDelta{}(b;SymmetricPoint(c;b))  fi 

---

Home Index