set A = { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } ;
set B = {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]};
thus { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } c= {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]} :: according to XBOOLE_0:def 10 :: thesis: {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]} c= { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } or a in {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]} )
assume a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } ; :: thesis: a in {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]}
then consider x, y being Integer such that
A1: a = [x,y] and
A2: ((2 * (x |^ 3)) + (x * y)) - 7 = 0 ;
A3: x |^ 3 = (x * x) * x by POLYEQ_5:2;
then x * (((2 * x) * x) + y) = 7 by A2;
then x divides 7 ;
then ( x = 1 or x = 7 or x = - 1 or x = - 7 ) by Th94, XPRIMES1:7;
hence a in {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]} by A1, A2, A3, ENUMSET1:def 2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]} or a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } )
assume a in {[1,5],[7,(- 97)],[(- 1),(- 9)],[(- 7),(- 99)]} ; :: thesis: a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 }

per cases then ( a = [1,5] or a = [7,(- 97)] or a = [(- 1),(- 9)] or a = [(- 7),(- 99)] ) by ENUMSET1:def 2;

suppose A4: a = [1,5] ; :: thesis: a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 }

((2 * (1 |^ 3)) + (1 * 5)) - 7 = 0 ;
hence a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } by A4; :: thesis: verum

end;

suppose A5: a = [7,(- 97)] ; :: thesis: a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 }

7 |^ 3 = (7 * 7) * 7 by POLYEQ_5:2;
then ((2 * (7 |^ 3)) + (7 * (- 97))) - 7 = 0 ;
hence a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } by A5; :: thesis: verum

end;

suppose A6: a = [(- 1),(- 9)] ; :: thesis: a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 }

(- 1) |^ 3 = ((- 1) * (- 1)) * (- 1) by POLYEQ_5:2;
then ((2 * ((- 1) |^ 3)) + ((- 1) * (- 9))) - 7 = 0 ;
hence a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } by A6; :: thesis: verum

end;

suppose A7: a = [(- 7),(- 99)] ; :: thesis: a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 }

(- 7) |^ 3 = ((- 7) * (- 7)) * (- 7) by POLYEQ_5:2;
then ((2 * ((- 7) |^ 3)) + ((- 7) * (- 99))) - 7 = 0 ;
hence a in { [x,y] where x, y is Integer : ((2 * (x |^ 3)) + (x * y)) - 7 = 0 } by A7; :: thesis: verum

end;

end;