theorem :: XREAL_1:134

for a, b being Real holds
( not a * b > 0 or ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )