theorem Th25: :: EUCLID_6:25

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