---

Step * of Lemma outer-Pasch-ext

∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| a_b_c} . ∀x:Point. ∀y:{y:Point| b-x-y} .
  (x # ab ⇒ (∃p:Point [(a_x_p ∧ c_p_y)]))
BY
{ Extract of Obid: outer-Pasch
  not unfolding  geo-SS geo-extend
  finishing with Auto
  normalizes to:
  
  λe,a,b,c,p,q,lsep. if lsep then geo-SS(e;a;p;q;c) else geo-SS(e;p;a;q;c) fi  }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a\_b\_c\}  .  \mforall{}x:Point.  \mforall{}y:\{y:Point|  b-x-y\}  .
    (x  \#  ab  {}\mRightarrow{}  (\mexists{}p:Point  [(a\_x\_p  \mwedge{}  c\_p\_y)]))


By

---

Latex:
Extract  of  Obid:  outer-Pasch
not  unfolding    geo-SS  geo-extend
finishing  with  Auto
normalizes  to:

\mlambda{}e,a,b,c,p,q,lsep.  if  lsep  then  geo-SS(e;a;p;q;c)  else  geo-SS(e;p;a;q;c)  fi 

---

Home Index