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