let r be real number ; :: thesis: for i being integer number st (- (PI / 2)) + ((2 * PI ) * i) < r & r < (PI / 2) + ((2 * PI ) * i) holds
cos r > 0
let i be integer number ; :: thesis: ( (- (PI / 2)) + ((2 * PI ) * i) < r & r < (PI / 2) + ((2 * PI ) * i) implies cos r > 0 )
assume ( (- (PI / 2)) + H₁(i) < r & r < (PI / 2) + H₁(i) ) ; :: thesis: cos r > 0
then ( ((- (PI / 2)) + H₁(i)) + (PI / 2) < r + (PI / 2) & r + (PI / 2) < ((PI / 2) + H₁(i)) + (PI / 2) ) by XREAL_1:8;
then A1: ( H₁(i) < r + (PI / 2) & r + (PI / 2) < PI + H₁(i) ) ;
sin (r + (PI / 2)) = cos r by SIN_COS:84;
hence cos r > 0 by A1, Th11; :: thesis: verum