for a being Nat ex k being Nat st
( a ^2 = 7 * k or a ^2 = (7 * k) + 1 or a ^2 = (7 * k) + 2 or a ^2 = (7 * k) + 4 )