theorem Th22: :: SIN_COS6:22

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