Step
*
of Lemma
lsep-inner-pasch-ext
∀e:OrientedPlane. ∀a,b:Point. ∀c:{c:Point| c # ab} . ∀p:{p:Point| a-p-c} . ∀q:{q:Point| b-q-c} .
  (∃x:{Point| (b_x_p ∧ a_x_q)})
BY
{ Extract of Obid: lsep-inner-pasch
  normalizes to:
  
  λe,a,b,c,p,q. if e "Lorsquashstable" c a b Ax then geo-SS(e;a;q;p;b) else geo-SS(e;b;p;q;a) fi 
  
  not unfolding  geo-SS
  finishing with Auto }
Latex:
Latex:
\mforall{}e:OrientedPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  c  \#  ab\}  .  \mforall{}p:\{p:Point|  a-p-c\}  .  \mforall{}q:\{q:Point|  b-q-c\}  .
    (\mexists{}x:\{Point|  (b\_x\_p  \mwedge{}  a\_x\_q)\})
By
Latex:
Extract  of  Obid:  lsep-inner-pasch
normalizes  to:
\mlambda{}e,a,b,c,p,q.  if  e  "Lorsquashstable"  c  a  b  Ax  then  geo-SS(e;a;q;p;b)  else  geo-SS(e;b;p;q;a)  fi 
not  unfolding    geo-SS
finishing  with  Auto
Home
Index