theorem Th147: :: NUMBER17:147

for s being positive Nat st s >= 3 holds
for f being Solution_of_Sierp169 of s holds rng (Solutions_of_Sierp168 f) c= { g where g is Solution_of_Sierp169 of s : verum }