assume 26 satisfies_Sierpinski_problem_86 ; :: thesis: contradiction

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

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

thus contradiction by A1, XPRIMES0:25; :: thesis: verum

end;

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

consider x, y being Prime such that
A3: x <> y and
A4: 25 = x * y by A2;
x divides x * y ;
then ( x = 1 or x = 5 or x = 25 ) by A4, Th10;
hence contradiction by A3, A4; :: thesis: verum

end;

end;