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