theorem Th90: :: SINCOS10:90
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
sec . (arcsec2 r) = r