theorem Th3: :: CATALAN1:3

for n being Nat st n > 1 holds
n < (2 * n) -' 1