theorem Th24: :: SIN_COS6:24

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