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