theorem :: XREAL_1:140

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