let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
angle (p1,p2,p3) = angle (c1,c2)
let c1, c2 be Element of COMPLEX ; :: thesis: ( c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) implies angle (p1,p2,p3) = angle (c1,c2) )
assume A1: ( c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) ) ; :: thesis: angle (p1,p2,p3) = angle (c1,c2)
thus angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2)) by EUCLID_3:35
.= angle (c1,c2) by A1, COMPLEX2:73, EUCLID_3:17 ; :: thesis: verum