theorem :: XREAL_1:144

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