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