theorem :: EUCLID_3:35

for p1, p2, p3 being Point of (TOP-REAL 2) holds angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2))