theorem :: NUMBER09:53

{ [x,y] where x, y is Nat : (y ^2) - (((x * (x + 1)) * (x + 2)) * (x + 3)) = 1 } = { [x,y] where x, y is Nat : y = ((x ^2) + (3 * x)) + 1 }