A1: sin is_differentiable_on ].(PI / 2),PI .[ by FDIFF_1:34, SIN_COS:73;
X: ].(PI / 2),PI .[ c= dom sin by SIN_COS:27;
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 th1 in ].(PI / 2),PI .[ ; :: thesis: 0 > diff sin ,th1
then ( PI / 2 < th1 & th1 < PI ) by XXREAL_1:4;
then ( (PI / 2) - (PI / 2) < th1 - (PI / 2) & th1 - (PI / 2) < PI - (PI / 2) ) by XREAL_1:11;
then A2: th1 - (PI / 2) in ].0 ,(PI / 2).[ by XXREAL_1:4;
A3: diff sin ,th1 = cos . ((PI / 2) + (th1 - (PI / 2))) by SIN_COS:73
.= - (sin . (th1 - (PI / 2))) by SIN_COS:83 ;
sin . (th1 - (PI / 2)) > 0 by A2, Lm2;
then 0 - (sin . (th1 - (PI / 2))) < 0 ;
hence 0 > diff sin ,th1 by A3; :: thesis: verum

end;

hence sin | ].(PI / 2),PI .[ is decreasing by A1, Lm1, X, ROLLE:10; :: thesis: verum