let r be Real; :: thesis: ( PI / 2 <= r & r <= PI & r / PI is rational & cos r is rational implies r in {(PI / 2),((2 * PI) / 3),PI} )
set R = PI - r;
assume ( PI / 2 <= r & r <= PI ) ; :: thesis: ( not r / PI is rational or not cos r is rational or r in {(PI / 2),((2 * PI) / 3),PI} )
then A1: ( PI - PI <= PI - r & PI - r <= PI - (PI / 2) ) by XREAL_1:13;
assume A2: ( r / PI is rational & cos r is rational ) ; :: thesis: r in {(PI / 2),((2 * PI) / 3),PI}
A3: (PI - r) / PI = (PI / PI) - (r / PI)
.= 1 - (r / PI) by XCMPLX_1:60 ;
cos (PI - r) = - (cos r) by EUCLID10:2;
then PI - r in {0,(PI / 3),(PI / 2)} by A1, A2, A3, Th53;
then ( PI - r = 0 or PI - r = PI / 3 or PI - r = PI / 2 ) by ENUMSET1:def 1;
hence r in {(PI / 2),((2 * PI) / 3),PI} by ENUMSET1:def 1; :: thesis: verum