for a, b being Nat st ( a mod 7 = 1 or a mod 7 = 2 or a mod 7 = 4 ) & ( b mod 7 = 1 or b mod 7 = 2 or b mod 7 = 4 ) holds
not not (a + b) mod 7 = 1 & ... & not (a + b) mod 7 = 6