let x be Real; :: thesis: ( 0 <= x & x < 2 * PI & sin x = 0 & not x = 0 implies x = PI )
assume that
A1: ( 0 <= x & x < 2 * PI ) and
A2: sin x = 0 ; :: thesis: ( x = 0 or x = PI )
sin . x = 0 by A2, SIN_COS:def 17;
then ( not x in ].0,PI.[ & not x in ].PI,(2 * PI).[ ) by Th7, Th9;
then ( x = 0 or ( x >= PI & PI >= x ) ) by A1, XXREAL_1:4;
hence ( x = 0 or x = PI ) by XXREAL_0:1; :: thesis: verum