:: deftheorem Def14 defines Solution_of_Sierp168 NUMBER15:def 14 :
for s being positive Nat
for b₂ being b₁ + 1 -element natural-valued positive-yielding FinSequence holds
( b₂ is Solution_of_Sierp168 of s iff b₂ is a_solution_of_Sierp168 );