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