theorem Th43: :: NUMBER13:43
for m, n being Nat st ( m is odd or m = (2 * n) + 1 ) holds
(2 |^ m) mod 3 = 2