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