theorem Th10: :: EUCLID_6:10

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