let n be Nat; :: 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:72;
then (2 - (3 / (n + 1))) - 2 >= 2 - 2 by XREAL_1:9;
then - (- (- (3 / (n + 1)))) >= 0 ;
hence contradiction by XREAL_1:139; :: thesis: verum