theorem Th52: :: NUMBER08:52

for n being Nat holds
( not n satisfies_Sierpinski_problem_86 or ( n - 1 is prime & ex x, y being Prime st
( x <> y & n + 1 = x * y ) ) or ( n + 1 is prime & ex x, y being Prime st
( x <> y & n - 1 = x * y ) ) )