let n be Nat; :: thesis: Catalan n is Integer

per cases ( n = 0 or n = 1 or n > 1 ) by NAT_1:25;

suppose n = 0 ; :: thesis: Catalan n is Integer

hence Catalan n is Integer ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: Catalan n is Integer

hence Catalan n is Integer ; :: thesis: verum

end;

suppose n > 1 ; :: thesis: Catalan n is Integer

then Catalan n = (4 * (((2 * n) -' 3) choose (n -' 1))) - (((2 * n) -' 1) choose (n -' 1)) by Th9;
hence Catalan n is Integer ; :: thesis: verum

end;

end;