theorem Th2: :: INTEGRA8:2

for x being Real
for n being Element of NAT holds sin (x + (((2 * n) + 1) * PI)) = - (sin x)