theorem Th8: :: CATALAN1:8

for n being Nat st n > 1 holds
Catalan n = (((2 * n) -' 2) !) / (((n -' 1) !) * (n !))