theorem Th11: :: EUCLID_6:11

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