theorem Th56: :: SIN_COS6:56
for i being Integer holds cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing