let r be Real; :: thesis: ( - 1 < r & r < 1 implies ( - (PI / 2) < arcsin r & arcsin r < PI / 2 ) )
assume A1: ( - 1 < r & r < 1 ) ; :: thesis: ( - (PI / 2) < arcsin r & arcsin r < PI / 2 )
then ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) by Th76;
then ( ( - (PI / 2) < arcsin r & arcsin r < PI / 2 ) or - (PI / 2) = arcsin r or arcsin r = PI / 2 ) by XXREAL_0:1;
hence ( - (PI / 2) < arcsin r & arcsin r < PI / 2 ) by A1, Th7, Th68, SIN_COS:77; :: thesis: verum