theorem Th8: :: EUCLID_6:8

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