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