theorem :: NUMBER13:51
for x, y, z, t being positive Nat holds ((4 |^ x) + (4 |^ y)) + (4 |^ z) <> 4 |^ t by Th50;