sin | [.((3 / 2) * PI),(2 * PI).] is one-to-one ;
hence sin | ].((3 / 2) * PI),(2 * PI).[ is one-to-one by Th2, XXREAL_1:25; :: thesis: verum