theorem :: NUMBER15:73

for S being positive Nat holds { f where f is Solution_of_Sierp168 of S : verum } is infinite