given x, y, z being Rational such that A1: (((((x ^2) + (y ^2)) + (z ^2)) + x) + y) + z = 1 ; :: thesis: contradiction
((((2 * x) + 1) ^2) + (((2 * y) + 1) ^2)) + (((2 * z) + 1) ^2) = 7 by A1;
hence contradiction by Th93; :: thesis: verum