let s be positive Nat; :: thesis: ( s >= 3 implies { f where f is Solution_of_Sierp169 of s : verum } is infinite )
assume A1: s >= 3 ; :: thesis: { f where f is Solution_of_Sierp169 of s : verum } is infinite
set F = Solutions_of_Sierp168 the Solution_of_Sierp169 of s;
A2: dom (Solutions_of_Sierp168 the Solution_of_Sierp169 of s) = NATPLUS by PARTFUN1:def 2;
rng (Solutions_of_Sierp168 the Solution_of_Sierp169 of s) c= { f where f is Solution_of_Sierp169 of s : verum } by A1, Th147;
hence { f where f is Solution_of_Sierp169 of s : verum } is infinite by A2, CARD_1:59; :: thesis: verum