let x, y, z, t be positive Nat; :: thesis: (((x / y) + (y / z)) + (z / t)) + (t / x) <> 1
( x / y >= 1 or y / z >= 1 or z / t >= 1 or t / x >= 1 )

proof

assume that
A1: ( x / y < 1 & y / z < 1 ) and
A2: z / t < 1 and
A3: t / x < 1 ; :: thesis: contradiction
A4: (x / y) * (y / z) = (x * y) / (y * z) by XCMPLX_1:76;
A5: (((x * y) * z) / ((y * z) * t)) * (t / x) = (((x * y) * z) * t) / (((y * z) * t) * x) by XCMPLX_1:76
.= 1 by XCMPLX_1:60 ;
A6: ((x / y) * (y / z)) * (z / t) = ((x * y) * z) / ((y * z) * t) by A4, XCMPLX_1:76;
(x / y) * (y / z) < 1 by A1, Th54;
then ((x / y) * (y / z)) * (z / t) < 1 by A2, A4, Th54;
hence contradiction by A3, A5, A6, Th54; :: thesis: verum

end;

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

suppose x / y >= 1 ; :: thesis: (((x / y) + (y / z)) + (z / t)) + (t / x) <> 1

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

end;

suppose y / z >= 1 ; :: thesis: (((x / y) + (y / z)) + (z / t)) + (t / x) <> 1

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

end;

suppose z / t >= 1 ; :: thesis: (((x / y) + (y / z)) + (z / t)) + (t / x) <> 1

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

end;

suppose t / x >= 1 ; :: thesis: (((x / y) + (y / z)) + (z / t)) + (t / x) <> 1

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

end;

end;