A1: sin is_differentiable_on ].0 ,(PI / 2).[ by FDIFF_1:34, SIN_COS:73;
X: ].0 ,(PI / 2).[ c= dom sin by SIN_COS:27;
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 A1, Lm1, X, ROLLE:9; :: thesis: verum