theorem Th105: :: SINCOS10:105

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