theorem Th1: :: HILB10_6:1

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)