theorem Th25: :: SIN_COS6:25

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