let c, b be real number ; :: thesis: ( ( for a being real number st a < 0 holds
c <= b - a ) implies b >= c )
assume A1: for a being real number st a < 0 holds
b - a >= c ; :: thesis: b >= c
assume b < c ; :: thesis: contradiction
then A2: 0 > b - c by Lm23;
set d = b - c;
A3: - (b - c) > 0 by A2;
then (- (b - c)) / 2 < - (b - c) by Lm30;
then b + (- ((b - c) / 2)) < b + (- (b - c)) by Lm10;
then A4: b - ((b - c) / 2) < b - (b - c) ;
(- (b - c)) / 2 > 0 by A3;
then - ((b - c) / 2) > 0 ;
then (b - c) / 2 < 0 ;
hence contradiction by A1, A4; :: thesis: verum