let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2))
( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) ) by Th15;
hence angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2)) by Th17, COMPLEX2:71; :: thesis: verum