let r be Real; :: thesis: ( 0 <= r & r <= 2 * PI & r / PI is rational & sin r is rational implies sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} )
assume A1: ( 0 <= r & r <= 2 * PI ) ; :: thesis: ( not r / PI is rational or not sin r is rational or sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} )
assume A2: ( r / PI is rational & sin r is rational ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}

per cases ( ( 0 <= r & r <= PI / 2 ) or ( PI / 2 <= r & r <= PI ) or ( PI <= r & r <= (3 * PI) / 2 ) or ( (3 * PI) / 2 <= r & r <= 2 * PI ) ) by A1;

suppose ( 0 <= r & r <= PI / 2 ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}

then r in {0,(PI / 6),(PI / 2)} by A2, Th62;
then ( r = 0 or r = PI / 6 or r = PI / 2 ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, SIN_COS:31, SIN_COS:77, EUCLID10:17; :: thesis: verum

end;

suppose ( PI / 2 <= r & r <= PI ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}

then r in {(PI / 2),((5 * PI) / 6),PI} by A2, Th64;
then ( r = PI / 2 or r = (5 * PI) / 6 or r = PI ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, Th5, SIN_COS:77; :: thesis: verum

end;

suppose ( PI <= r & r <= (3 * PI) / 2 ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}

then r in {PI,((7 * PI) / 6),((3 * PI) / 2)} by A2, Th66;
then ( r = PI or r = (7 * PI) / 6 or r = (3 * PI) / 2 ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, Th7, SIN_COS:77; :: thesis: verum

end;

suppose ( (3 * PI) / 2 <= r & r <= 2 * PI ) ; :: thesis: sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))}

then r in {((3 * PI) / 2),((11 * PI) / 6),(2 * PI)} by A2, Th68;
then ( r = (3 * PI) / 2 or r = (11 * PI) / 6 or r = 2 * PI ) by ENUMSET1:def 1;
hence sin r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, Th9, SIN_COS:77; :: thesis: verum

end;

end;