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 = b - c;
assume b > c ; :: thesis: contradiction
then A2: 0 < b - c by Lm21;
then c + ((b - c) / 2) < c + (b - c) by Lm10, Lm27;
then c < b - ((b - c) / 2) by Lm19;
hence contradiction by A1, A2; :: thesis: verum