theorem Th1: :: CATALAN1:1

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