set A = { n where n is odd Nat : n divides (3 |^ n) + 1 } ;
thus { n where n is odd Nat : n divides (3 |^ n) + 1 } c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= { n where n is odd Nat : n divides (3 |^ n) + 1 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is odd Nat : n divides (3 |^ n) + 1 } or x in {1} )
assume x in { n where n is odd Nat : n divides (3 |^ n) + 1 } ; :: thesis: x in {1}
then consider n being odd Nat such that
A1: n = x and
A2: n divides (3 |^ n) + 1 ;
n = 1

proof

assume A3: n <> 1 ; :: thesis: contradiction
A4: (3 * 3) |^ n = (3 |^ n) * (3 |^ n) by NEWTON:7;
((3 |^ n) ^2) - (1 ^2) = ((3 |^ n) - 1) * ((3 |^ n) + 1) ;
then A5: n divides (9 |^ n) - 1 by A2, A4, INT_2:2;
defpred S₁[ Nat] means ( $1 is odd & 1 < $1 & $1 divides (9 |^ $1) - 1 );
A6: ex k being Nat st S₁[k] by A3, A5, NAT_1:25;
consider N being Nat such that
A7: S₁[N] and
A8: for n being Nat st S₁[n] holds
N <= n from NAT_1:sch 5(A6);
reconsider N = N as odd Element of NAT by A7, ORDINAL1:def 12;
set E = Euler N;
set d = N gcd (Euler N);
A9: 1 mod N = 1 by A7, NAT_D:14;
reconsider k = (9 |^ N) - 1 as Nat ;
9,N are_coprime by A7, Th45;
then (9 |^ (Euler N)) mod N = 1 by A7, EULER_2:18;
then ((9 |^ (Euler N)) - 1) mod N = (1 - 1) mod N by A9, INT_6:7
.= 0 ;
then N divides (9 |^ (Euler N)) - 1 by INT_1:62;
then A10: N divides ((9 |^ N) - 1) gcd ((9 |^ (Euler N)) - 1) by A7, INT_2:def 2;
A11: ((9 |^ N) - 1) gcd ((9 |^ (Euler N)) - 1) = (9 |^ (N gcd (Euler N))) - 1 by Th26;

A12: now :: thesis: not N gcd (Euler N) <= 1

assume N gcd (Euler N) <= 1 ; :: thesis: contradiction
then ( N gcd (Euler N) < 1 or N gcd (Euler N) = 1 ) by XXREAL_0:1;
then N in {1,2,4,8} by A10, A11, Th12, NAT_1:14;
then ( N = 2 * 1 or N = 2 * 2 or N = 2 * 4 ) by A7, ENUMSET1:def 2;
hence contradiction ; :: thesis: verum

end;

A13: N gcd (Euler N) <= Euler N by Th13;
A14: N gcd (Euler N) divides N by INT_2:def 2;
A15: Euler N <= N - 1 by A7, EULER_1:19;
N - 1 < N - 0 by XREAL_1:15;
then Euler N < N by A15, XXREAL_0:2;
then N gcd (Euler N) < N by A13, XXREAL_0:2;
hence contradiction by A8, A14, A12, A10, A11, INT_2:9; :: thesis: verum

end;

hence x in {1} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in { n where n is odd Nat : n divides (3 |^ n) + 1 } )
assume x in {1} ; :: thesis: x in { n where n is odd Nat : n divides (3 |^ n) + 1 }
then A16: x = 1 by TARSKI:def 1;
A17: 1 = (2 * 0) + 1 ;
1 divides (3 |^ 1) + 1 by INT_2:12;
hence x in { n where n is odd Nat : n divides (3 |^ n) + 1 } by A16, A17; :: thesis: verum