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