theorem Th19: :: CATALAN1:19
for n being Nat st n > 0 holds
Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n)