let x be real number ; :: thesis: ( x in ].((3 / 2) * PI ),(2 * PI ).[ implies cos . x > 0 )
assume x in ].((3 / 2) * PI ),(2 * PI ).[ ; :: thesis: cos . x > 0
then ( (3 / 2) * PI < x & x < 2 * PI ) by XXREAL_1:4;
then ( ((3 / 2) * PI ) - PI < x - PI & x - PI < (2 * PI ) - PI ) by XREAL_1:11;
then ( PI / 2 < x - PI & x - PI < (3 / 2) * PI ) by Lm6, XXREAL_0:2;
then A1: x - PI in ].(PI / 2),((3 / 2) * PI ).[ by XXREAL_1:4;
cos . (x - PI ) = cos . (- (PI - x))
.= cos . (PI + (- x)) by SIN_COS:33
.= - (cos . (- x)) by SIN_COS:83
.= - (cos . x) by SIN_COS:33 ;
hence cos . x > 0 by A1, Th29; :: thesis: verum