theorem Th6: :: NUMBER05:6
for a being Integer holds
( 3 divides a or (a |^ 3) mod 9 = 1 or (a |^ 3) mod 9 = 8 )