theorem :: HILB10_5:21

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