theorem :: NIVEN:63

for r being Real
for i being Integer st (2 * PI) * i <= r & r <= (PI / 2) + ((2 * PI) * i) & r / PI is rational & sin r is rational holds
r in {((2 * PI) * i),((PI / 6) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i))}