for a, b being Nat st 7 divides (a ^2) + (b ^2) holds
( 7 divides a & 7 divides b )