theorem Th62: :: NIVEN:62

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