for r being Real holds
( ( - (sqrt 2) <= r & r <= - 1 & arccosec1 r = - (PI / 2) implies r = - 1 ) & ( - (sqrt 2) <= r & r <= - 1 & arccosec1 r = - (PI / 4) implies r = - (sqrt 2) ) ) by Th32, Th91;