theorem :: XREAL_1:133

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