A1: PI / 2 < PI by Lm6, XXREAL_1:2;
A2: arcsec2 . (- 1) = arcsec2 (- 1)
.= PI by A1, Th31, Th70 ;
A3: ( PI / 2 < (3 / 4) * PI & (3 / 4) * PI <= PI ) by Lm6, XXREAL_1:2;
arcsec2 . (- (sqrt 2)) = arcsec2 (- (sqrt 2))
.= (3 / 4) * PI by A3, Th31, Th70 ;
hence ( arcsec2 . (- (sqrt 2)) = (3 / 4) * PI & arcsec2 . (- 1) = PI ) by A2; :: thesis: verum