theorem Th27: :: EUCLID_6:27

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 & p <> p2 holds
angle (p,p3,p2) >= angle (p1,p3,p2)