theorem :: SIN_COS6:44

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