theorem :: NIVEN:15
for i being Integer holds cos (((4 * PI) / 3) + ((2 * PI) * i)) = - (1 / 2) by COMPLEX2:9, Th11;