A1: for x being Real st x in ].0,PI.[ holds
diff (cos,x) < 0

proof

let x be Real; :: thesis: ( x in ].0,PI.[ implies diff (cos,x) < 0 )
assume x in ].0,PI.[ ; :: thesis: diff (cos,x) < 0
then 0 < sin . x by Th7;
then 0 - (sin . x) < 0 ;
hence diff (cos,x) < 0 by SIN_COS:67; :: thesis: verum

end;

].0,PI.[ is open by RCOMP_1:7;
hence cos | ].0,PI.[ is decreasing by A1, FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:67; :: thesis: verum