given x, y, z being positive Nat such that A1: ((x / y) + (y / z)) + (z / x) = 1 ; :: thesis: contradiction
DD: ((x / y) * (y / z)) * (z / x) = 1 by Multiply1;
( not x / y < 1 or not y / z < 1 or not z / x < 1 )

proof

assume D1: ( x / y < 1 & y / z < 1 & z / x < 1 ) ; :: thesis: contradiction
then (x / y) * (y / z) < 1 by XREAL_1:162;
hence contradiction by DD, D1, XREAL_1:162; :: thesis: verum

end;

per cases then ( x / y >= 1 or y / z >= 1 or z / x >= 1 ) ;

suppose x / y >= 1 ; :: thesis: contradiction

then (x / y) + (y / z) > 1 + 0 by XREAL_1:8;
hence contradiction by A1, XREAL_1:8; :: thesis: verum

end;

suppose y / z >= 1 ; :: thesis: contradiction

then (x / y) + (y / z) > 1 + 0 by XREAL_1:8;
hence contradiction by A1, XREAL_1:8; :: thesis: verum

end;

suppose z / x >= 1 ; :: thesis: contradiction

then (z / x) + (y / z) > 1 + 0 by XREAL_1:8;
then (x / y) + ((y / z) + (z / x)) > 0 + 1 by XREAL_1:8;
hence contradiction by A1; :: thesis: verum

end;

end;