let n be natural number ; :: thesis: ( n > 0 implies Catalan n > 0 )
assume A1: n > 0 ; :: thesis: Catalan n > 0
defpred S₁[ Nat] means Catalan $1 > 0 ;
A2: S₁[1] by Th11;
A3: for n being non empty Nat st S₁[n] holds
S₁[n + 1] by Th16;
A4: for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A2, A3);
n is non empty Nat by A1;
hence Catalan n > 0 by A4; :: thesis: verum