for i being Integer holds sin (((11 * PI) / 6) + ((2 * PI) * i)) = - (1 / 2) by COMPLEX2:8, Th9;