let t be Real; :: thesis: ( t in ].(- PI),0.[ implies sin . t < 0 )
assume t in ].(- PI),0.[ ; :: thesis: sin . t < 0
then ( - PI < t & t < 0 ) by XXREAL_1:4;
then ( - 0 < - t & - t < - (- PI) ) by XREAL_1:24;
then - t in ].0,PI.[ ;
then 0 < sin . (- t) by COMPTRIG:7;
then 0 < - (sin . t) by SIN_COS:30;
hence sin . t < 0 ; :: thesis: verum