let r be Real; :: thesis: ( - (sqrt 2) < r & r < - 1 implies ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) )
assume A1: ( - (sqrt 2) < r & r < - 1 ) ; :: thesis: ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI )
then ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) by Th106;
then ( ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) or (3 / 4) * PI = arcsec2 r or arcsec2 r = PI ) by XXREAL_0:1;
hence ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) by A1, Th31, Th90; :: thesis: verum