theorem Th23: :: SIN_COS6:23

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