theorem Th54: :: SIN_COS6:54

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