theorem Th30: :: CATALAN2:30

for k being Nat holds card (Domin_0 ((2 + k),1)) = k + 1