theorem :: SIN_COS6:41

for r being Real
for i being Integer st (2 * PI) * i < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r < 1