theorem Th15: :: SIN_COS6:15
for r being Real
for i being Integer st ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds
cos r > 0