theorem :: XREAL_1:137

for a, b being Real st 0 <= a & b <= 0 holds
a / b <= 0 ;