theorem :: SIN_COS6:40

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