theorem :: XREAL_1:135

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