cos | [.0 ,PI .] is one-to-one ;
hence cos | ].0 ,PI .[ is one-to-one by Lm18, Th2; :: thesis: verum