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