theorem :: NUMBER15:77

for x, y, z, t being positive Nat holds
( not (x ^2) + (2 * (y ^2)) = z ^2 or not (2 * (x ^2)) + (y ^2) = t ^2 )