theorem :: NUMBER03:36

for n being Nat holds
( (2 |^ n) mod 3 = 1 or (2 |^ n) mod 3 = 2 )