let r be Real; :: thesis: ( 1 < r & r < sqrt 2 implies ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) )
assume A1: ( 1 < r & r < sqrt 2 ) ; :: thesis: ( 0 < arcsec1 r & arcsec1 r < PI / 4 )
then arcsec1 r <= PI / 4 by Th105;
then ( ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) or 0 = arcsec1 r or arcsec1 r = PI / 4 ) by A1, Th105, XXREAL_0:1;
hence ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) by A1, Th31, Th89; :: thesis: verum