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