Nuprl Definition : hp-angle-sum
abc + xyz ≅ def ==  ∃p,p',d',f':Point. (((abc ≅a dep ∧ fep ≅a xyz) ∧ e_p'_p) ∧ (out(e dd') ∧ out(e ff')) ∧ d'-p'-f')
Definitions occuring in Statement : 
geo-out: out(p ab)
, 
geo-cong-angle: abc ≅a xyz
, 
geo-strict-between: a-b-c
, 
geo-between: a_b_c
, 
geo-point: Point
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
Definitions occuring in definition : 
exists: ∃x:A. B[x]
, 
geo-point: Point
, 
geo-cong-angle: abc ≅a xyz
, 
geo-between: a_b_c
, 
and: P ∧ Q
, 
geo-out: out(p ab)
, 
geo-strict-between: a-b-c
FDL editor aliases : 
hp-angle-sum
Latex:
abc  +  xyz  \mcong{}  def  ==
    \mexists{}p,p',d',f':Point.  (((abc  \mcong{}\msuba{}  dep  \mwedge{}  fep  \mcong{}\msuba{}  xyz)  \mwedge{}  e\_p'\_p)  \mwedge{}  (out(e  dd')  \mwedge{}  out(e  ff'))  \mwedge{}  d'-p'-f')
Date html generated:
2019_10_16-PM-02_02_40
Last ObjectModification:
2019_05_31-PM-02_31_57
Theory : euclidean!plane!geometry
Home
Index