theorem Th72: :: NUMBER15:72

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