A1: cos is_differentiable_on ].0 ,(PI / 2).[ by FDIFF_1:34, SIN_COS:72;
X: ].0 ,(PI / 2).[ c= dom cos by SIN_COS:27;
for th being Real st th in ].0 ,(PI / 2).[ holds
diff cos ,th < 0

proof

let th be Real; :: thesis: ( th in ].0 ,(PI / 2).[ implies diff cos ,th < 0 )
assume A2: th in ].0 ,(PI / 2).[ ; :: thesis: diff cos ,th < 0
A3: diff cos ,th = - (sin . th) by SIN_COS:72;
0 < sin . th by A2, Lm2;
then 0 - (sin . th) < 0 ;
hence diff cos ,th < 0 by A3; :: thesis: verum

end;

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