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