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:67;
hence diff (cos,th) < 0 ; :: thesis: verum

end;

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