let r be real number ; :: thesis: ( - 1 <= r & r <= 1 implies ( 0 <= (arccos r) / (2 * PI ) & (arccos r) / (2 * PI ) <= 1 / 2 ) )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: ( 0 <= (arccos r) / (2 * PI ) & (arccos r) / (2 * PI ) <= 1 / 2 )
then ( 0 <= arccos r & arccos r <= PI ) by SIN_COS6:101;
then ( 0 / (2 * PI ) <= (arccos r) / (2 * PI ) & (arccos r) / (2 * PI ) <= (1 * PI ) / (2 * PI ) ) by XREAL_1:74;
hence ( 0 <= (arccos r) / (2 * PI ) & (arccos r) / (2 * PI ) <= 1 / 2 ) by XCMPLX_1:92; :: thesis: verum