A1: arccosec2 . 1 = arccosec2 1
.= PI / 2 by Th32, Th72 ;
A2: PI / 4 <= PI / 2 by Lm8, XXREAL_1:2;
arccosec2 . (sqrt 2) = arccosec2 (sqrt 2)
.= PI / 4 by A2, Th32, Th72 ;
hence ( arccosec2 . (sqrt 2) = PI / 4 & arccosec2 . 1 = PI / 2 ) by A1; :: thesis: verum