let a, b, c be Integer; :: thesis: ( a + 2 < b implies ((c - b) + 1) + 2 < (c - a) + 1 )
assume A1: a + 2 < b ; :: thesis: ((c - b) + 1) + 2 < (c - a) + 1
assume ((c - b) + 1) + 2 >= (c - a) + 1 ; :: thesis: contradiction
then ((c - b) + 3) - 3 >= ((c - a) + 1) - 3 by XREAL_1:9;
then c - b >= c - (a + 2) ;
hence contradiction by A1, XREAL_1:10; :: thesis: verum