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