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