theorem Th7: :: CATALAN1:7
for n being Nat holds 2 * (2 - (3 / (n + 1))) < 4