theorem Th26: :: EUCLID_6:26

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