let x be Real; :: 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:1;
then ( x = PI or x = 2 * PI or ( PI < x & x < 2 * PI ) ) by XXREAL_0:1;
then ( x = PI or x = 2 * PI or x in ].PI,(2 * PI).[ ) by XXREAL_1:4;
hence sin . x <= 0 by Th9, SIN_COS:76; :: thesis: verum