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 Th19;
hence angle p1,p2,p3 = angle (p1 - p2),(0. (TOP-REAL 2)),(p3 - p2) by Th21, COMPLEX2:85; :: thesis: verum