theorem :: EUCLID_3:37

for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p1,p2,p3) <> 0 holds
angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))