theorem :: NUMBER09:52
for x, y, z being Nat holds ((x ^2) - (2 * (y ^2))) + (8 * z) <> 3