let n be Nat; :: thesis: for a, b, c being Integer
for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) >= (b * (p . i2)) + c } is diophantine Subset of ()

let a, b, c be Integer; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) >= (b * (p . i2)) + c } is diophantine Subset of ()
let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : a * (p . i1) >= (b * (p . i2)) + c } is diophantine Subset of ()
defpred S1[ XFinSequence of NAT ] means a * (\$1 . i1) > (b * (\$1 . i2)) + c;
defpred S2[ XFinSequence of NAT ] means a * (\$1 . i1) = (b * (\$1 . i2)) + c;
defpred S3[ XFinSequence of NAT ] means ( S1[\$1] or S2[\$1] );
defpred S4[ XFinSequence of NAT ] means a * (\$1 . i1) >= (b * (\$1 . i2)) + c;
A1: { p where p is n -element XFinSequence of NAT : S1[p] } is diophantine Subset of () by Th7;
A2: { p where p is n -element XFinSequence of NAT : S2[p] } is diophantine Subset of () by Th6;
A3: { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } is diophantine Subset of () from A4: for p being n -element XFinSequence of NAT holds
( S3[p] iff S4[p] ) by XXREAL_0:1;
{ p where p is n -element XFinSequence of NAT : S3[p] } = { q where q is n -element XFinSequence of NAT : S4[q] } from hence { p where p is n -element XFinSequence of NAT : a * (p . i1) >= (b * (p . i2)) + c } is diophantine Subset of () by A3; :: thesis: verum