theorem Th85: :: SINCOS10:85

for x being set st x in [.1,(sqrt 2).] holds
arcsec1 . x in [.0,(PI / 4).]