for th being Real st th in ].((3 / 2) * PI),(2 * PI).[ holds
diff (cos,th) > 0

proof

let th be Real; :: thesis: ( th in ].((3 / 2) * PI),(2 * PI).[ implies diff (cos,th) > 0 )
assume A1: th in ].((3 / 2) * PI),(2 * PI).[ ; :: thesis: diff (cos,th) > 0
th < 2 * PI by A1, XXREAL_1:4;
then A2: th - ((3 / 2) * PI) < (2 * PI) - ((3 / 2) * PI) by XREAL_1:9;
A3: diff (cos,th) = - (sin . (PI + ((PI / 2) + (th - ((3 / 2) * PI))))) by SIN_COS:67
.= - (- (sin . ((PI / 2) + (th - ((3 / 2) * PI))))) by SIN_COS:78
.= cos . (th - ((3 / 2) * PI)) by SIN_COS:78 ;
(3 / 2) * PI < th by A1, XXREAL_1:4;
then ((3 / 2) * PI) - ((3 / 2) * PI) < th - ((3 / 2) * PI) by XREAL_1:9;
then th - ((3 / 2) * PI) in ].0,(PI / 2).[ by A2, XXREAL_1:4;
hence diff (cos,th) > 0 by A3, SIN_COS:80; :: thesis: verum

end;

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