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 arcsin (- r) = - (arcsin (- (- r))) by Th78
.= (arccos r) - (PI / 2) by A2 ;
hence (arccos r) - (arcsin (- r)) = PI / 2 ; :: thesis: verum