let r be Real; :: thesis: ( 0 <= r & r <= PI / 2 & r / PI is rational & sin r is rational implies r in {0,(PI / 6),(PI / 2)} )
set t = (PI / 2) - r;
assume 0 <= r ; :: thesis: ( not r <= PI / 2 or not r / PI is rational or not sin r is rational or r in {0,(PI / 6),(PI / 2)} )
then A1: (PI / 2) - r <= (PI / 2) - 0 by XREAL_1:10;
assume r <= PI / 2 ; :: thesis: ( not r / PI is rational or not sin r is rational or r in {0,(PI / 6),(PI / 2)} )
then A2: (PI / 2) - (PI / 2) <= (PI / 2) - r by XREAL_1:10;
assume A3: ( r / PI is rational & sin r is rational ) ; :: thesis: r in {0,(PI / 6),(PI / 2)}
A4: ((PI / 2) - r) / PI = ((PI / 2) / PI) - (r / PI) ;
A5: (PI / 2) / PI = 1 / 2 by XCMPLX_1:203;
cos ((PI / 2) - r) = ((cos (PI / 2)) * (cos r)) + ((sin (PI / 2)) * (sin r)) by SIN_COS:83
.= sin r by SIN_COS:77 ;
then (PI / 2) - r in {0,(PI / 3),(PI / 2)} by A1, A2, A3, A4, A5, Th53;
then ( (PI / 2) - r = 0 or (PI / 2) - r = PI / 3 or (PI / 2) - r = PI / 2 ) by ENUMSET1:def 1;
hence r in {0,(PI / 6),(PI / 2)} by ENUMSET1:def 1; :: thesis: verum