theorem :: SIN_COS6:80

for r, s being Real st s <= 0 & (r ^2) + (s ^2) = 1 holds
cos (arcsin r) = - s