theorem Th4: :: INTEGRA8:4

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