theorem :: EUCLID_3:47

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