for r being Real holds
( not sin r = 0 or r = (2 * PI) * [\(r / (2 * PI))/] or r = PI + ((2 * PI) * [\(r / (2 * PI))/]) )