theorem :: SIN_COS6:103

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