let r be Real; :: thesis: ( - (2 * PI) < r & r < 0 implies sin (r / 2) <> 0 )
assume A1: ( - (2 * PI) < r & r < 0 ) ; :: thesis: sin (r / 2) <> 0
assume A2: sin (r / 2) = 0 ; :: thesis: contradiction
( 0 * (- 1) < r * (- 1) & r * (- 1) < (- (2 * PI)) * (- 1) ) by A1, XREAL_1:69;
then A3: sin ((- r) / 2) <> 0 by Th4;
reconsider r0 = r / 2 as Real ;
sin (- r0) = - (sin r0) by SIN_COS:31;
hence contradiction by A2, A3; :: thesis: verum