theorem :: HILB10_5:20
for n being Nat
for A being Subset of (n -xtuples_of NAT) st A is diophantine holds
A is recursively_enumerable