:: deftheorem defines satisfies_Sierpinski_problem_86 NUMBER08:def 5 :
for n being Nat holds
( n satisfies_Sierpinski_problem_86 iff ex p1, p2, p3 being Prime st
( p1,p2,p3 are_mutually_distinct & (n |^ 2) - 1 = (p1 * p2) * p3 ) );