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