for r being Real st 0 <= r & r <= 2 * PI & sin r = - 1 holds
r = (3 / 2) * PI