theorem :: SIN_COS6:61

for r, s being Real
for i being Integer st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s & s < (2 * PI) + ((2 * PI) * i) & sin r = sin s & cos r = cos s holds
r = s