:: deftheorem defines satisfies_Sierpinski_problem_87b NUMBER07:def 3 :
for n being Nat holds
( n satisfies_Sierpinski_problem_87b iff ex a, b, c being odd Prime st
( a,b,c are_mutually_distinct & (n |^ 2) + 1 = (a * b) * c ) );