### Nuprl Definition : eu-cong-angle

`abc = xyz ==`
`  (¬(a = b ∈ Point))`
`  ∧ (¬(c = b ∈ Point))`
`  ∧ (¬(x = y ∈ Point))`
`  ∧ (¬(z = y ∈ Point))`
`  ∧ (∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ y_x_x' ∧ y_z_z' ∧ ba'=yx' ∧ bc'=yz' ∧ a'c'=x'z'))`

Definitions occuring in Statement :  eu-between-eq: `a_b_c` eu-congruent: `ab=cd` eu-point: `Point` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions occuring in definition :  not: `¬A` equal: `s = t ∈ T` exists: `∃x:A. B[x]` eu-point: `Point` eu-between-eq: `a_b_c` and: `P ∧ Q` eu-congruent: `ab=cd`
FDL editor aliases :  eu-conga

Latex:
abc  =  xyz  ==
(\mneg{}(a  =  b))
\mwedge{}  (\mneg{}(c  =  b))
\mwedge{}  (\mneg{}(x  =  y))
\mwedge{}  (\mneg{}(z  =  y))
\mwedge{}  (\mexists{}a',c',x',z':Point.  (b\_a\_a'  \mwedge{}  b\_c\_c'  \mwedge{}  y\_x\_x'  \mwedge{}  y\_z\_z'  \mwedge{}  ba'=yx'  \mwedge{}  bc'=yz'  \mwedge{}  a'c'=x'z'))

Date html generated: 2016_06_16-PM-01_31_55
Last ObjectModification: 2016_05_20-PM-02_09_20

Theory : euclidean!geometry

Home Index