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