theorem :: NUMBER02:31

for n being Nat holds
( not 3 divides n iff ex k being Nat st
( n = (3 * k) + 1 or n = (3 * k) + 2 ) )