theorem Th16: :: EUCLID_6:16

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