let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies (arccos (- r)) - (arcsin r) = PI / 2 )
assume A1: ( - 1 <= r & r <= 1 ) ; :: thesis: (arccos (- r)) - (arcsin r) = PI / 2
then A2: (arcsin r) + (arccos r) = (PI / 2) + 0 by Th108;
( - (- 1) >= - r & - r >= - 1 ) by A1, XREAL_1:24;
then arccos (- r) = PI - (arccos (- (- r))) by Th101
.= (arcsin r) + (PI / 2) by A2 ;
hence (arccos (- r)) - (arcsin r) = PI / 2 ; :: thesis: verum