theorem Th8: :: BORSUK_7:8

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