theorem :: NIVEN:61

for r being Real st r / PI is rational & cos r is rational holds
cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))}