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 th in ].0 ,(PI / 2).[ ; :: thesis: diff cos ,th < 0
then 0 < sin . th by Lm1;
then ( diff cos ,th = - (sin . th) & 0 - (sin . th) < 0 ) by SIN_COS:72;
hence diff cos ,th < 0 ; :: thesis: verum

end;

hence cos | ].0 ,(PI / 2).[ is decreasing by FDIFF_1:34, ROLLE:10, SIN_COS:27, SIN_COS:72; :: thesis: verum