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