theorem Th27: :: CATALAN2:27

for m, n being Nat st 2 * (m + 1) <= n holds
card ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1)))) = card (Choose (n,m,1,0))