theorem Th22: :: HILB10_3:22

for n being Nat
for a, b, c being Integer
for i1, i2, i3 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : [(a * (p . i1)),(b * (p . i2))] is Pell's_solution of ((c * (p . i3)) ^2) -' 1 } is diophantine Subset of (n -xtuples_of NAT)