theorem Th23: :: NUMBER02:23

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