theorem Th109: :: SINCOS10:109

for r being Real st 1 < r & r < sqrt 2 holds
( 0 < arcsec1 r & arcsec1 r < PI / 4 )