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