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 + H₁(i) < r & r < (2 * PI) + H₁(i) ) ; :: thesis: sin r < 0
then ( (PI + H₁(i)) - H₁(i) < r - H₁(i) & r - H₁(i) < ((2 * PI) + H₁(i)) - H₁(i) ) by XREAL_1:9;
then r - H₁(i) in ].PI,(2 * PI).[ by XXREAL_1:4;
then sin . (r + H₁( - i)) < 0 by COMPTRIG:9;
then sin . r < 0 by Th8;
hence sin r < 0 by SIN_COS:def 17; :: thesis: verum