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