theorem Th26: :: SIN_COS6:26

for r being Real st cos r = 1 holds
r = (2 * PI) * [\(r / (2 * PI))/]