theorem Th53: :: NIVEN:53

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