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