let n be Nat; :: thesis: card (Domin_0 ((2 * n),n)) = Catalan (n + 1)
A1: Catalan (n + 1) = (((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1) by CATALAN1:def 1;
( ((2 * n) + 2) -' 2 = ((2 * n) + 2) - 2 & (n + 1) -' 1 = (n + 1) - 1 ) by XREAL_0:def 2;
hence card (Domin_0 ((2 * n),n)) = Catalan (n + 1) by A1, Th33; :: thesis: verum