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