let n be natural number ; :: thesis: ( n > 0 implies Catalan (n + 1) < 4 * (Catalan n) )
assume A1: n > 0 ; :: thesis: Catalan (n + 1) < 4 * (Catalan n)
then A2: Catalan n > 0 ;
Catalan (n + 1) = (2 * (2 - (3 / (n + 1)))) * (Catalan n) by A1, Th19;
hence Catalan (n + 1) < 4 * (Catalan n) by A2, Th7, XREAL_1:70; :: thesis: verum