set n = 2;
thus (3 * (2 |^ (2 |^ 2))) + 1 is composite by Lm2, Lm4, XPRIMES0:49; :: according to NUMBER13:def 5 :: thesis: for m being positive Nat st m < 2 holds
not (3 * (2 |^ (2 |^ m))) + 1 is composite
let m be positive Nat; :: thesis: ( m < 2 implies not (3 * (2 |^ (2 |^ m))) + 1 is composite )
assume m < 2 ; :: thesis: not (3 * (2 |^ (2 |^ m))) + 1 is composite

per cases then ( m = 0 or m = 1 ) by NAT_1:23;

suppose m = 0 ; :: thesis: not (3 * (2 |^ (2 |^ m))) + 1 is composite

hence not (3 * (2 |^ (2 |^ m))) + 1 is composite ; :: thesis: verum

end;

suppose m = 1 ; :: thesis: not (3 * (2 |^ (2 |^ m))) + 1 is composite

hence not (3 * (2 |^ (2 |^ m))) + 1 is composite by Lm2, XPRIMES1:13; :: thesis: verum

end;

end;