for n being Nat
for i being Element of n holds { p where p is b₁ -element XFinSequence of NAT : p . i > 1 } is diophantine Subset of (n -xtuples_of NAT)