theorem Th28: :: CATALAN2:28

for m, n being Nat st 2 * (m + 1) <= n holds
card (Domin_0 (n,(m + 1))) = (n choose (m + 1)) - (n choose m)