theorem Th55: :: NIVEN:55

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