theorem :: EUCLID_6:48

for p1, p2, p3 being Point of (TOP-REAL 2)
for c1, c2 being Element of COMPLEX st c1 = euc2cpx (p1 - p2) & c2 = euc2cpx (p3 - p2) holds
angle (p1,p2,p3) = angle (c1,c2) by Lm7;