for a being Nat holds
( 7 divides a or (a ^2) mod 7 = 1 or (a ^2) mod 7 = 2 or (a ^2) mod 7 = 4 )