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