let p1, p2, p3 be Point of (TOP-REAL 2); :: thesis: angle p1,p2,p3 = angle (p1 - p2),(0.REAL 2),(p3 - p2)
A1: (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) by Th19;
(euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) by Th19;
hence angle p1,p2,p3 = angle (p1 - p2),(0.REAL 2),(p3 - p2) by A1, Th21, COMPLEX2:85; :: thesis: verum