1023 = 3 * 341 ;
then 2 |^ 10,1 are_congruent_mod 3 by Lm10;
then (2 |^ 10) |^ 56,1 |^ 56 are_congruent_mod 3 by GR_CY_3:34;
then (2 |^ 560) * (2 |^ 1),1 * 2 are_congruent_mod 3 by Lm1119, INT_4:11;
hence 3 divides (2 |^ 561) - 2 by Lm1121; :: thesis: verum