theorem :: XREAL_1:143

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