theorem :: XREAL_1:87

for a, b being Real st b < 0 & a < b holds
b " < a " by Lm31;