let a, b be real number ; :: 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 ) )
a / b = a * (b " ) by XCMPLX_0:def 9;
then b " <> 0 by A1;
then ( a <> 0 & b <> 0 ) by A1;
hence ( ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) ) by A1; :: thesis: verum