assume 8 satisfies_Sierpinski_problem_86 ; :: thesis: contradiction

per cases then ( ( 8 - 1 is prime & ex x, y being Prime st
( x <> y & 8 + 1 = x * y ) ) or ( 8 + 1 is prime & ex x, y being Prime st
( x <> y & 8 - 1 = x * y ) ) ) by Th52;

suppose that 8 - 1 is prime and
A1: ex x, y being Prime st
( x <> y & 8 + 1 = x * y ) ; :: thesis: contradiction

consider x, y being Prime such that
A2: x <> y and
A3: x * y = 9 by A1;
x divides x * y ;
then ( x = 1 or x = 3 or x = 9 ) by A3, Th9;
hence contradiction by A2, A3; :: thesis: verum

end;

suppose that 8 + 1 is prime and
A4: ex x, y being Prime st
( x <> y & 8 - 1 = x * y ) ; :: thesis: contradiction

thus contradiction by A4, XPRIMES1:7; :: thesis: verum

end;

end;