theorem Th59: :: NIVEN:59

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