theorem :: NUMBER02:44

( not 6 divides (2 |^ 6) - 2 & 6 divides (3 |^ 6) - 3 & ( for n being Nat holds
( not n < 6 or n divides (2 |^ n) - 2 or not n divides (3 |^ n) - 3 ) ) )