let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 )
then r in [.(- 1),1.] by XXREAL_1:1;
then arcsin . r in rng arcsin by Th63, FUNCT_1:def 3;
hence ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) by Th62, XXREAL_1:1; :: thesis: verum