for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, r being Real st p1 in circle (a,b,r) & p2 in circle (a,b,r) & p3 in circle (a,b,r) & p4 in circle (a,b,r) & p1 <> p3 & p1 <> p4 & p2 <> p3 & p2 <> p4 & not angle (p1,p3,p2) = angle (p1,p4,p2) & not angle (p1,p3,p2) = (angle (p1,p4,p2)) - PI holds
angle (p1,p3,p2) = (angle (p1,p4,p2)) + PI