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