let n be Nat; :: thesis: Catalan n is Element of NAT
Catalan n is Integer by Th13;
hence Catalan n is Element of NAT by INT_1:3; :: thesis: verum