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