let r be Real; :: thesis: ( - (sqrt 2) <= r & r <= - 1 implies ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) )
assume ( - (sqrt 2) <= r & r <= - 1 ) ; :: thesis: ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI )
then A1: r in [.(- (sqrt 2)),(- 1).] ;
then r in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) by Th46, RELAT_1:62;
then (arcsec2 | [.(- (sqrt 2)),(- 1).]) . r in rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) by FUNCT_1:def 3;
then arcsec2 r in rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) by A1, FUNCT_1:49;
hence ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) by Th98, XXREAL_1:1; :: thesis: verum