let a, b, c be real number ; :: thesis: ( 0 <= a & b < c implies b - a < c )
assume ( 0 <= a & b < c ) ; :: thesis: b - a < c
then b + 0 < a + c by Th42;
hence b - a < c by Lm17; :: thesis: verum