theorem :: XREAL_1:141

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