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