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