theorem Th60: :: SIN_COS6:60

for i being Integer holds cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is one-to-one