set A = { [x,y,z] where x, y, z is positive Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } ;
set B = {[1,1,1]};
thus { [x,y,z] where x, y, z is positive Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } c= {[1,1,1]} :: according to XBOOLE_0:def 10 :: thesis: {[1,1,1]} c= { [x,y,z] where x, y, z is positive 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 positive Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } or a in {[1,1,1]} )
assume a in { [x,y,z] where x, y, z is positive Integer : ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) } ; :: thesis: a in {[1,1,1]}
then consider x, y, z being positive Integer such that
A1: a = [x,y,z] and
A2: ( ((x / y) + (y / z)) + (z / x) = 3 & x,y,z are_mutually_coprime ) ;
( x = 1 & y = 1 & z = 1 ) by A2, Th108;
hence a in {[1,1,1]} by A1, TARSKI:def 1; :: thesis: verum

end;

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