theorem Th5: :: EUCLID13:5

for r being Real st - (2 * PI) < r & r < 0 holds
sin (r / 2) <> 0