let n be Nat; :: thesis: ( n satisfies_Sierpinski_problem_86 implies n is even )
assume A1: n satisfies_Sierpinski_problem_86 ; :: thesis: n is even
assume n is odd ; :: thesis: contradiction
then A2: ( n - 1 is even & n + 1 is even ) ;
( n - 1 is prime or n + 1 is prime ) by A1, Th52;
then ( n - 1 = 2 or n + 1 = 2 ) by A2;
then ( n = 3 or n = 1 ) ;
hence contradiction by A1, Th50; :: thesis: verum