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