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:80;
hence 0 < diff (sin,th) by SIN_COS:68; :: thesis: verum

end;

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