let r be Real; :: thesis: ( 0 < r & r < 2 * PI implies sin (r / 2) <> 0 )
assume A1: ( 0 < r & r < 2 * PI ) ; :: thesis: sin (r / 2) <> 0
assume A2: sin (r / 2) = 0 ; :: thesis: contradiction
consider i0 being Integer such that
A3: r / 2 = PI * i0 by A2, BORSUK_7:7;
A4: r = (2 * i0) * PI by A3;
reconsider p = 2 * PI as Real ;
( 0 < i0 * p & i0 * p < p ) by A1, A4;
then i0 = 1 by Th1;
hence contradiction by A1, A3; :: thesis: verum