assume 6 satisfies_Sierpinski_problem_86 ; :: thesis: contradiction

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

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

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

end;

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

thus contradiction by A2, XPRIMES1:5; :: thesis: verum

end;

end;