A1: arcsec1 . 1 = arcsec1 1
.= 0 by Th31, Th69 ;
A2: PI / 4 < PI / 2 by Lm5, XXREAL_1:3;
arcsec1 . (sqrt 2) = arcsec1 (sqrt 2)
.= PI / 4 by A2, Th31, Th69 ;
hence ( arcsec1 . 1 = 0 & arcsec1 . (sqrt 2) = PI / 4 ) by A1; :: thesis: verum