theorem Th4: :: EUCLID_6:4

for p1, p2, p3, p4 being Point of (TOP-REAL 2) holds
( (angle (p1,p4,p2)) + (angle (p2,p4,p3)) = angle (p1,p4,p3) or (angle (p1,p4,p2)) + (angle (p2,p4,p3)) = (angle (p1,p4,p3)) + (2 * PI) )