theorem :: NIVEN:9

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