let x, y, z be positive Nat; :: thesis: ( ((x / y) + (y / z)) + (z / x) = 3 implies ( x = y & y = z ) )
assume A1: ((x / y) + (y / z)) + (z / x) = 3 ; :: thesis: ( x = y & y = z )
B2: ( x / y = y / z & y / z = z / x )

proof

assume D1: ( x / y <> y / z or y / z <> z / x ) ; :: thesis: contradiction
set a = x / y;
set b = y / z;
set c = z / x;
((((x / y) + (y / z)) + (z / x)) / 3) |^ 3 > ((x / y) * (y / z)) * (z / x) by SERIES3, D1;
hence contradiction by A1, Multiply1; :: thesis: verum

end;

then b1: (x / y) * y = 1 * y by A1;
(y / z) * z = 1 * z by A1, B2;
hence ( x = y & y = z ) by b1, XCMPLX_1:87; :: thesis: verum