let b1, b2, c be Nat; :: thesis: ( b2 <= c implies b2 - b1 <= c )
assume b2 <= c ; :: thesis: b2 - b1 <= c
then A1: b2 - b1 <= c - b1 by XREAL_1:9;
c - b1 <= c by Th3;
hence b2 - b1 <= c by A1, XXREAL_0:2; :: thesis: verum