set A = { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } ;
set B = {[1,1,1],[(- 1),(- 1),(- 1)]};
thus { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } c= {[1,1,1],[(- 1),(- 1),(- 1)]} :: according to XBOOLE_0:def 10 :: thesis: {[1,1,1],[(- 1),(- 1),(- 1)]} c= { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } or a in {[1,1,1],[(- 1),(- 1),(- 1)]} )
assume a in { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } ; :: thesis: a in {[1,1,1],[(- 1),(- 1),(- 1)]}
then consider x, y, z being non zero Integer such that
A1: a = [x,y,z] and
A2: ((x / y) + (y / z)) + (z / x) = 3 and
A3: x,y,z are_mutually_coprime ;
( ( x = 1 or x = - 1 ) & ( y = 1 or y = - 1 ) & ( z = 1 or z = - 1 ) ) by A2, A3, Th108;
hence a in {[1,1,1],[(- 1),(- 1),(- 1)]} by A1, A2, TARSKI:def 2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {[1,1,1],[(- 1),(- 1),(- 1)]} or a in { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } )
assume a in {[1,1,1],[(- 1),(- 1),(- 1)]} ; :: thesis: a in { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) }
then A4: ( a = [1,1,1] or a = [(- 1),(- 1),(- 1)] ) by TARSKI:def 2;
A5: 1,1,1 are_mutually_coprime by WSIERP_1:9;
- 1, - 1, - 1 are_mutually_coprime by Th11, WSIERP_1:9;
hence a in { [x,y,z] where x, y, z is non zero Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } by A4, A5, Lm14, Lm15; :: thesis: verum