theorem :: NUMBER17:87
( ( for x, y, z being positive Nat holds (x / y) + (y / z) <> z / x ) iff for u, v, w being positive Nat holds (u |^ 3) + (v |^ 3) <> w |^ 3 )