theorem Th34: :: CATALAN2:34

for n being Nat holds card (Domin_0 ((2 * n),n)) = Catalan (n + 1)