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