set A = { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) } ;
set B = {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]};
A1: (- 5) |^ 3 = ((- 5) * (- 5)) * (- 5) by POLYEQ_5:2;
A2: 4 |^ 3 = (4 * 4) * 4 by POLYEQ_5:2;
thus { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) } c= {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} :: according to XBOOLE_0:def 10 :: thesis: {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} c= { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) } or a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} )
assume a in { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) } ; :: thesis: a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]}
then consider x, y, z being Integer such that
A3: a = [x,y,z] and
A4: (x + y) + z = 3 and
A5: ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ;
A6: 3 |^ 3 = (3 * 3) * 3 by POLYEQ_5:2;
( x |^ 3 = (x * x) * x & y |^ 3 = (y * y) * y & z |^ 3 = (z * z) * z & ((x + y) + z) |^ 3 = (((x + y) + z) * ((x + y) + z)) * ((x + y) + z) ) by POLYEQ_5:2;
then (((x + y) + z) |^ 3) - (((x |^ 3) + (y |^ 3)) + (z |^ 3)) = ((3 * (x + y)) * (x + z)) * (y + z) ;
then 27 - 3 = ((3 * (x + y)) * (x + z)) * (y + z) by A4, A5, A6;
then A7: 8 = ((x + y) * (x + z)) * (y + z)
.= ((3 - z) * (3 - y)) * (3 - x) by A4 ;
then A8: ((3 - x) * (3 - y)) * (3 - z) = 8 ;
((3 - z) + (3 - y)) + (3 - x) = 2 * 3 by A4;

per cases then ( ( 3 - z is even & 3 - y is even & 3 - x is even ) or ( 3 - z is even & 3 - y is odd & 3 - x is odd ) or ( 3 - z is odd & 3 - y is even & 3 - x is odd ) or ( 3 - z is odd & 3 - y is odd & 3 - x is even ) ) ;

suppose ( 3 - z is even & 3 - y is even & 3 - x is even ) ; :: thesis: a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]}

then ( ( 3 - x = 2 & 3 - y = 2 & 3 - z = 2 ) or ( 3 - x = - 2 & 3 - y = - 2 & 3 - z = 2 ) or ( 3 - x = - 2 & 3 - y = 2 & 3 - z = - 2 ) or ( 3 - x = 2 & 3 - y = - 2 & 3 - z = - 2 ) ) by A7, Lm11;
hence a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} by A3, A4, ENUMSET1:def 2; :: thesis: verum

end;

suppose ( 3 - z is even & 3 - y is odd & 3 - x is odd ) ; :: thesis: a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]}

then ( ( 3 - z = 8 & 3 - y = 1 & 3 - x = 1 ) or ( 3 - z = 8 & 3 - y = - 1 & 3 - x = - 1 ) or ( 3 - z = - 8 & 3 - y = 1 & 3 - x = - 1 ) or ( 3 - z = - 8 & 3 - y = - 1 & 3 - x = 1 ) ) by A7, Lm12;
hence a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} by A3, A4, ENUMSET1:def 2; :: thesis: verum

end;

suppose ( 3 - z is odd & 3 - y is even & 3 - x is odd ) ; :: thesis: a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]}

then ( ( 3 - y = 8 & 3 - z = 1 & 3 - x = 1 ) or ( 3 - y = 8 & 3 - z = - 1 & 3 - x = - 1 ) or ( 3 - y = - 8 & 3 - z = 1 & 3 - x = - 1 ) or ( 3 - y = - 8 & 3 - z = - 1 & 3 - x = 1 ) ) by A7, Lm12;
hence a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} by A3, A4, ENUMSET1:def 2; :: thesis: verum

end;

suppose ( 3 - z is odd & 3 - y is odd & 3 - x is even ) ; :: thesis: a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]}

then ( ( 3 - x = 8 & 3 - y = 1 & 3 - z = 1 ) or ( 3 - x = 8 & 3 - y = - 1 & 3 - z = - 1 ) or ( 3 - x = - 8 & 3 - y = 1 & 3 - z = - 1 ) or ( 3 - x = - 8 & 3 - y = - 1 & 3 - z = 1 ) ) by A8, Lm12;
hence a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} by A3, A4, ENUMSET1:def 2; :: thesis: verum

end;

end;

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} or a in { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) } )
assume a in {[1,1,1],[(- 5),4,4],[4,(- 5),4],[4,4,(- 5)]} ; :: thesis: a in { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) }
then A9: ( a = [1,1,1] or a = [(- 5),4,4] or a = [4,(- 5),4] or a = [4,4,(- 5)] ) by ENUMSET1:def 2;
( ((- 5) + 4) + 4 = 3 & (4 + 4) + (- 5) = 3 & ((1 |^ 3) + (1 |^ 3)) + (1 |^ 3) = 3 & ((4 |^ 3) + ((- 5) |^ 3)) + (4 |^ 3) = 3 & ((4 |^ 3) + (4 |^ 3)) + ((- 5) |^ 3) = 3 ) by A1, A2;
hence a in { [x,y,z] where x, y, z is Integer : ( (x + y) + z = 3 & ((x |^ 3) + (y |^ 3)) + (z |^ 3) = 3 ) } by A9; :: thesis: verum