let a be odd Nat; :: thesis: 3 divides (2 |^ a) + 1
reconsider n = (a - 1) / 2 as Nat ;
3 divides (2 |^ ((2 * n) + 1)) - 2 by NEWTON02:173;
then 3 divides ((2 |^ ((2 * n) + 1)) - 2) + 3 by WSIERP_1:4;
hence 3 divides (2 |^ a) + 1 ; :: thesis: verum