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