for r, s being Real st cos r = cos s holds
ex i being Integer st
( r = s + ((2 * PI) * i) or r = (- s) + ((2 * PI) * i) )