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