let a, b be real number ; :: thesis: ( a " < 0 & b " <= a " implies a <= b )
assume ( a " < 0 & a " >= b " ) ; :: thesis: a <= b
then (a " ) " <= (b " ) " by Lm37;
hence a <= b ; :: thesis: verum