for b being Nat holds
( 3 divides b or 3 divides b - 1 or 3 divides b + 1 )