let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies ( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 ) )

assume that

A1: - 1 <= r and

A2: r <= 1 ; :: thesis: ( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 )

arccos r <= PI by A1, A2, SIN_COS6:99;

then A3: (arccos r) / (2 * PI) <= (1 * PI) / (2 * PI) by XREAL_1:72;

0 <= arccos r by A1, A2, SIN_COS6:99;

hence ( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 ) by A3, XCMPLX_1:91; :: thesis: verum

assume that

A1: - 1 <= r and

A2: r <= 1 ; :: thesis: ( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 )

arccos r <= PI by A1, A2, SIN_COS6:99;

then A3: (arccos r) / (2 * PI) <= (1 * PI) / (2 * PI) by XREAL_1:72;

0 <= arccos r by A1, A2, SIN_COS6:99;

hence ( 0 <= (arccos r) / (2 * PI) & (arccos r) / (2 * PI) <= 1 / 2 ) by A3, XCMPLX_1:91; :: thesis: verum