let r be Real; :: thesis: for i being Integer st PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds
sin r <= 0
let i be Integer; :: thesis: ( PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) implies sin r <= 0 )
assume ( PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) ) ; :: thesis: sin r <= 0
then ( ( PI + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) ) or PI + ((2 * PI) * i) = r or r = (2 * PI) + ((2 * PI) * i) ) by XXREAL_0:1;
hence sin r <= 0 by Th12, COMPLEX2:8, SIN_COS:77; :: thesis: verum