A1: arccosec1 . (- 1) = arccosec1 (- 1)
.= - (PI / 2) by Th32, Th71 ;
A2: - (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3;
arccosec1 . (- (sqrt 2)) = arccosec1 (- (sqrt 2))
.= - (PI / 4) by A2, Th32, Th71 ;
hence ( arccosec1 . (- 1) = - (PI / 2) & arccosec1 . (- (sqrt 2)) = - (PI / 4) ) by A1; :: thesis: verum