theorem Th57: :: NIVEN:57

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