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