let r be real number ; :: 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 Th110;
( - (- 1) >= - r & - r >= - 1 ) by A1, XREAL_1:26;
then arcsin (- r) = - (arcsin (- (- r))) by Th79
.= (arccos r) - (PI / 2) by A2 ;
hence (arccos r) - (arcsin (- r)) = PI / 2 ; :: thesis: verum