let a, b, c be Real; :: thesis: ( a < b implies (c - b) + 1 < (c - a) + 1 )
assume a < b ; :: thesis: (c - b) + 1 < (c - a) + 1
then c - b < c - a by XREAL_1:10;
hence (c - b) + 1 < (c - a) + 1 by XREAL_1:6; :: thesis: verum