Domin_0 (n,m) c= Choose (n,m,1,0) by Th21;
hence Domin_0 (n,m) is finite ; :: thesis: verum