:: deftheorem Def18 defines Solution_of_Sierp169 NUMBER17:def 18 :
for s being positive Nat st s >= 3 holds
for b₂ being b₁ + 1 -element natural-valued positive-yielding FinSequence holds
( b₂ is Solution_of_Sierp169 of s iff b₂ is a_solution_of_Sierp169 );