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

proof

let x be Real; :: thesis: ( x in ].PI,(2 * PI).[ implies diff (cos,x) > 0 )
assume x in ].PI,(2 * PI).[ ; :: thesis: diff (cos,x) > 0
then 0 - (sin . x) > 0 by Th9, XREAL_1:50;
hence diff (cos,x) > 0 by SIN_COS:67; :: thesis: verum

end;

].PI,(2 * PI).[ is open by RCOMP_1:7;
hence cos | ].PI,(2 * PI).[ is increasing by A1, FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:67; :: thesis: verum