theorem Th2: :: CATALAN1:2

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