theorem :: NUMBER17:148

for s being positive Nat st s >= 3 holds
{ f where f is Solution_of_Sierp169 of s : verum } is infinite