theorem Th50: :: NUMBER13:50

for n, x, y, z, t being positive Nat holds
( ((n |^ x) + (n |^ y)) + (n |^ z) = n |^ t iff ( ( n = 2 & y = x & z = x + 1 & t = x + 2 ) or ( n = 2 & y = x + 1 & z = x & t = x + 2 ) or ( n = 2 & z = y & x = y + 1 & t = y + 2 ) or ( n = 3 & y = x & z = x & t = x + 1 ) ) )