assume 28 satisfies_Sierpinski_problem_86 ; :: thesis: contradiction

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

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

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

end;

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

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

end;

end;