theorem :: NUMBER18:65
for x, y, z being positive Nat holds not ((x |^ 3) + (y |^ 3)) + (z |^ 3) = ((2 * x) * y) * z