theorem :: NIVEN:58

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