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

proof

let th be Real; :: thesis: ( th in ].0 ,(PI / 2).[ implies 0 < diff sin ,th )
assume th in ].0 ,(PI / 2).[ ; :: thesis: 0 < diff sin ,th
then cos . th > 0 by SIN_COS:85;
hence 0 < diff sin ,th by SIN_COS:73; :: thesis: verum

end;

hence sin | ].0 ,(PI / 2).[ is increasing by FDIFF_1:34, ROLLE:9, SIN_COS:27, SIN_COS:73; :: thesis: verum