theorem Th21: :: CATALAN2:21

for m, n being Nat holds Domin_0 (n,m) c= Choose (n,m,1,0)