theorem :: SINCOS10:102

for r being Real holds
( ( - (sqrt 2) <= r & r <= - 1 & arcsec2 r = (3 / 4) * PI implies r = - (sqrt 2) ) & ( - (sqrt 2) <= r & r <= - 1 & arcsec2 r = PI implies r = - 1 ) ) by Th31, Th90;