theorem Th9: :: CATALAN1:9

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