let x, y, z, t be positive Nat; :: thesis: ( (x ^2) + (5 * (y ^2)) <> z ^2 or (5 * (x ^2)) + (y ^2) <> t ^2 )
assume ( (x ^2) + (5 * (y ^2)) = z ^2 & (5 * (x ^2)) + (y ^2) = t ^2 ) ; :: thesis: contradiction
then ex x1, y1, z1, t1 being Nat st
( (x1 ^2) + (5 * (y1 ^2)) = z1 ^2 & (5 * (x1 ^2)) + (y1 ^2) = t1 ^2 & x1,y1 are_coprime ) by Lm19;
hence contradiction by Lm20; :: thesis: verum