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