let r be real number ; :: thesis: ( - 1 <= r & r <= 1 implies ( 0 <= arccos r & arccos r <= PI ) )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: ( 0 <= arccos r & arccos r <= PI )
then r in [.(- 1),1.] by XXREAL_1:1;
then arccos . r in rng arccos by Th88, FUNCT_1:def 3;
hence ( 0 <= arccos r & arccos r <= PI ) by Th87, XXREAL_1:1; :: thesis: verum