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