theorem :: NIVEN:70

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