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