let r be Real; :: thesis: for i being Integer st (2 * PI) * i < r & r < PI + ((2 * PI) * i) holds
sin r > 0
let i be Integer; :: thesis: ( (2 * PI) * i < r & r < PI + ((2 * PI) * i) implies sin r > 0 )
assume ( H₁(i) < r & r < PI + H₁(i) ) ; :: thesis: sin r > 0
then ( H₁(i) - H₁(i) < r - H₁(i) & r - H₁(i) < (PI + H₁(i)) - H₁(i) ) by XREAL_1:9;
then r - H₁(i) in ].0,PI.[ by XXREAL_1:4;
then sin . (r + H₁( - i)) > 0 by COMPTRIG:7;
then sin . r > 0 by Th8;
hence sin r > 0 by SIN_COS:def 17; :: thesis: verum