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