let a, b be real number ; :: 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 ( a <> 0 & b <> 0 ) ;
hence ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1; :: thesis: verum