theorem Th4: :: EUCLID13:4

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