theorem :: XREAL_1:138

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