let r be Real; :: thesis: ( 0 <= r & r <= 2 * PI & r / PI is rational & cos r is rational implies cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))} )
assume A1: ( 0 <= r & r <= 2 * PI ) ; :: thesis: ( not r / PI is rational or not cos r is rational or cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))} )
assume A2: ( r / PI is rational & cos r is rational ) ; :: thesis: cos 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: cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))}

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

end;

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

then r in {(PI / 2),((2 * PI) / 3),PI} by A2, Th55;
then ( r = PI / 2 or r = (2 * PI) / 3 or r = PI ) by ENUMSET1:def 1;
hence cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by ENUMSET1:def 3, SIN_COS:77, EUCLID10:23; :: thesis: verum

end;

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

then r in {PI,((4 * PI) / 3),((3 * PI) / 2)} by A2, Th57;
then ( r = PI or r = (4 * PI) / 3 or r = (3 * PI) / 2 ) by ENUMSET1:def 1;
hence cos r in {0,1,(- 1),(1 / 2),(- (1 / 2))} by Th11, ENUMSET1:def 3, SIN_COS:77; :: thesis: verum

end;

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

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

end;

end;