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