theorem Th17: :: COMPTRIG:17

for x being Real st 0 <= x & x < 2 * PI & sin x = 0 & not x = 0 holds
x = PI