theorem :: NUMBER02:50

for a, b being Nat st ex k being Nat st
( a = (7 * k) + 1 or a = (7 * k) + 2 or a = (7 * k) + 4 ) & ex k being Nat st
( b = (7 * k) + 1 or b = (7 * k) + 2 or b = (7 * k) + 4 ) holds
ex k being Nat st