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