set x = (5 |^ 4) + ((5 + 1) |^ 4);
thus 2 <= (5 |^ 4) + ((5 + 1) |^ 4) by Lm6, Lm7; :: according to NUMBER02:def 1 :: thesis: ( not (5 |^ 4) + ((5 + 1) |^ 4) is prime & ( for n being Nat holds
( not n < 5 or not (n |^ 4) + ((n + 1) |^ 4) is composite ) ) )
(5 |^ 4) + ((5 + 1) |^ 4) = 17 * 113 by Lm6, Lm7;
hence not (5 |^ 4) + ((5 + 1) |^ 4) is prime by Th13, PEPIN:60; :: thesis: for n being Nat holds
( not n < 5 or not (n |^ 4) + ((n + 1) |^ 4) is composite )
given n being Nat such that A1: n < 5 and
A2: (n |^ 4) + ((n + 1) |^ 4) is composite ; :: thesis: contradiction
n <= 5 - 1 by A1, INT_1:52;
then not not n = 0 & ... & not n = 4 ;
hence contradiction by A2, Th56, Th57, Th58, Th59; :: thesis: verum