:: deftheorem Def12 defines Sierp45FS NUMBER14:def 12 :
for a, b, c being Integer st a,b,c are_mutually_distinct holds
for b₄ being FinSequence of INT holds
( b₄ is Sierp45FS of a,b,c iff ex h being Integer ex F being FinSequence of NAT st
( h = ((a - b) * (a - c)) * (b - c) & F = Sgm (PrimeDivisors>3 h) & len b₄ = len F & ( for i being object st i in dom b₄ holds
( not F . i divides a + (b₄ . i) & not F . i divides b + (b₄ . i) & not F . i divides c + (b₄ . i) ) ) ) );