let r be Real; :: thesis: ( 1 < r & r < sqrt 2 implies ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) )
assume A1: ( 1 < r & r < sqrt 2 ) ; :: thesis: ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 )
then ( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 ) by Th108;
then ( ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) or PI / 4 = arccosec2 r or arccosec2 r = PI / 2 ) by XXREAL_0:1;
hence ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) by A1, Th32, Th92; :: thesis: verum