for r being Real st cos ((2 * PI) * r) = 1 holds
r in INT