let r be Real; :: thesis: ( - 1 < r & r < 1 implies ( 0 < arccos r & arccos r < PI ) )
assume A1: ( - 1 < r & r < 1 ) ; :: thesis: ( 0 < arccos r & arccos r < PI )
then arccos r <= PI by Th99;
then ( ( 0 < arccos r & arccos r < PI ) or 0 = arccos r or arccos r = PI ) by A1, Th99, XXREAL_0:1;
hence ( 0 < arccos r & arccos r < PI ) by A1, Th91, SIN_COS:31, SIN_COS:77; :: thesis: verum