theorem :: NUMBER17:85

for x, y being positive Nat holds
( ((x * y) + x) + y = 2 |^ 32 iff ( ( x = 640 & y = 6700416 ) or ( x = 6700416 & y = 640 ) ) )