theorem :: XREAL_1:86

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