theorem Th28: :: HILB10_4:28

for n being Nat
for a, b being Integer
for c being Nat
for i1, i2, i3 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : ( a * (p . i1) = [\((b * (p . i2)) / (c * (p . i3)))/] & c * (p . i3) <> 0 ) } is diophantine Subset of (n -xtuples_of NAT)