theorem :: SIN_COS6:18
for r being Real
for i being Integer st (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) holds
cos r >= 0