theorem :: EUCLID_6:19

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