theorem Th29: :: HILB10_4:29

for n being Nat
for i1, i2, i3 being Element of n st n <> 0 holds
{ p where p is b₁ -element XFinSequence of NAT : ( p . i1 >= p . i3 & p . i2 = (p . i1) choose (p . i3) ) } is diophantine Subset of (n -xtuples_of NAT)