theorem Th13: :: EUCLID_6:13

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