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