let x, y, z, t be non zero Integer; :: thesis: ( (x ^2) + (6 * (y ^2)) <> z ^2 or (6 * (x ^2)) + (y ^2) <> t ^2 )
( |.x.| ^2 = x ^2 & |.y.| ^2 = y ^2 & |.z.| ^2 = z ^2 & |.t.| ^2 = t ^2 ) by COMPLEX1:75;
hence ( (x ^2) + (6 * (y ^2)) <> z ^2 or (6 * (x ^2)) + (y ^2) <> t ^2 ) by Lm24; :: thesis: verum