theorem :: CATALAN1:21

for n being Nat st n > 0 holds
Catalan (n + 1) < 4 * (Catalan n)