theorem Th55: :: SIN_COS6:55

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