for th1 being Real st th1 in ].(PI / 2),PI.[ holds
0 > diff (sin,th1)

proof

let th1 be Real; :: thesis: ( th1 in ].(PI / 2),PI.[ implies 0 > diff (sin,th1) )
assume A1: th1 in ].(PI / 2),PI.[ ; :: thesis: 0 > diff (sin,th1)
then th1 < PI by XXREAL_1:4;
then A2: th1 - (PI / 2) < PI - (PI / 2) by XREAL_1:9;
PI / 2 < th1 by A1, XXREAL_1:4;
then (PI / 2) - (PI / 2) < th1 - (PI / 2) by XREAL_1:9;
then th1 - (PI / 2) in ].0,(PI / 2).[ by A2, XXREAL_1:4;
then sin . (th1 - (PI / 2)) > 0 by Lm1;
then A3: 0 - (sin . (th1 - (PI / 2))) < 0 ;
diff (sin,th1) = cos . ((PI / 2) + (th1 - (PI / 2))) by SIN_COS:68
.= - (sin . (th1 - (PI / 2))) by SIN_COS:78 ;
hence 0 > diff (sin,th1) by A3; :: thesis: verum

end;

hence sin | ].(PI / 2),PI.[ is decreasing by FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:68; :: thesis: verum