let r be Real; :: 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 Th86, FUNCT_1:def 3;
hence ( 0 <= arccos r & arccos r <= PI ) by Th85, XXREAL_1:1; :: thesis: verum