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

proof

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

end;

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