theorem Th97: :: SINCOS10:97

rng (arcsec1 | [.1,(sqrt 2).]) = [.0,(PI / 4).]