theorem Th13: :: SIN_COS6:13
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