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:44
.= angle c1,c2 by A1, COMPLEX2:87, EUCLID_3:21 ; :: thesis: verum