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