let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies arccos r = PI - (arccos (- r)) )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: arccos r = PI - (arccos (- r))
then A1: ( - (- 1) >= - r & - r >= - 1 ) by XREAL_1:24;
then 0 + (arccos (- r)) <= PI by Th99;
then A2: 0 <= PI - (arccos (- r)) by XREAL_1:19;
0 <= arccos (- r) by A1, Th99;
then PI + 0 <= PI + (arccos (- r)) by XREAL_1:6;
then A3: PI - (arccos (- r)) <= PI by XREAL_1:20;
r = (- 1) * (- r)
.= ((cos PI) * (cos (arccos (- r)))) + ((sin PI) * (sin (arccos (- r)))) by A1, Th91, SIN_COS:77
.= cos (PI - (arccos (- r))) by COMPLEX2:3 ;
hence arccos r = PI - (arccos (- r)) by A2, A3, Th92; :: thesis: verum