let n be natural number ; :: thesis: 2 * (2 - (3 / (n + 1))) < 4
assume 2 * (2 - (3 / (n + 1))) >= 4 ; :: thesis: contradiction
then (2 * (2 - (3 / (n + 1)))) / 2 >= 4 / 2 by XREAL_1:74;
then (2 - (3 / (n + 1))) - 2 >= 2 - 2 by XREAL_1:11;
then - (- (- (3 / (n + 1)))) >= 0 ;
then 3 / (n + 1) <= 0 ;
hence contradiction by XREAL_1:141; :: thesis: verum