Nuprl Lemma : straight-angle-sum2

∀e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k:Point.  (abc + xyz ≅ ijk ⇒ out(y xz) ⇒ (a-b-c ⇐⇒ i-j-k))


Proof

Error : references
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z,i,j,k:Point.    (abc  +  xyz  \mcong{}  ijk  {}\mRightarrow{}  out(y  xz)  {}\mRightarrow{}  (a-b-c  \mLeftarrow{}{}\mRightarrow{}  i-j-k))


Date html generated: 2020_05_21-AM-10_25_27
Last ObjectModification: 2019_06_22-PM-10_48_48

Theory : euclidean!plane!geometry


Home Index