let r be real number ; :: thesis: for i being integer number st (2 * PI ) * i < r & r < PI + ((2 * PI ) * i) holds
sin r > 0
let i be integer number ; :: 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:11;
then r - H₁(i) in ].0 ,PI .[ by XXREAL_1:4;
then sin . (r + H₁( - i)) > 0 by COMPTRIG:23;
then sin . r > 0 by Th8;
hence sin r > 0 by SIN_COS:def 21; :: thesis: verum