let n be Nat; :: thesis: 9 divides (2 |^ (6 * n)) - 1
(9 * 7) + 1,1 are_congruent_mod 9 ;
then (2 |^ 6) |^ n,1 |^ n are_congruent_mod 9 by Lm5, GR_CY_3:34;
hence 9 divides (2 |^ (6 * n)) - 1 by NEWTON:9; :: thesis: verum