let a, b, c be Real; :: thesis: ( 0 <= a & b <= c implies b - a <= c )
assume that
A1: 0 <= a and
A2: b <= c ; :: thesis: b - a <= c
b + 0 <= a + c by A1, A2, Th38;
hence b - a <= c by Lm18; :: thesis: verum