theorem :: SIN_COS6:19

for r being Real
for i being Integer st (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) holds
cos r <= 0