let a, b be Real; :: thesis: ( not a / b < 0 or ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) )
assume A1: a / b < 0 ; :: thesis: ( ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) )
then A2: a <> 0 ;
a / b = a * (b ") by XCMPLX_0:def 9;
then b " <> 0 by A1;
hence ( ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) ) by A1, A2; :: thesis: verum