set A = { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } ;
set B = { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) } ;
thus { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } c= { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) } :: according to XBOOLE_0:def 10 :: thesis: { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) } c= { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 }

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } or q in { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) } )
assume q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } ; :: thesis: q in { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) }
then consider x, y, z, t being positive Integer such that
A1: q = [x,y,z,t] and
A2: (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 ;
(((x / y) * (y / z)) * (z / t)) * (t / x) = (4 / 4) |^ 4 by Lm18;
then ( x / y = y / z & y / z = z / t & z / t = t / x ) by A2, Th99;
then ( x = y & y = z & z = t ) by A2, XCMPLX_1:58;
hence q in { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) } by A1; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) } or q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } )
assume q in { [x,y,z,t] where x, y, z, t is positive Integer : ( x = y & y = z & z = t ) } ; :: thesis: q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 }
then consider x, y, z, t being positive Integer such that
A3: q = [x,y,z,t] and
A4: ( x = y & y = z & z = t ) ;
( x / y = 1 & y / z = 1 & z / t = 1 & t / x = 1 ) by A4, XCMPLX_1:60;
then (((x / y) + (y / z)) + (z / t)) + (t / x) = ((1 + 1) + 1) + 1 ;
hence q in { [x,y,z,t] where x, y, z, t is positive Integer : (((x / y) + (y / z)) + (z / t)) + (t / x) = 4 } by A3; :: thesis: verum