theorem Th8: :: CLOSURE1:8

for I being set
for M being non-empty ManySortedSet of I
for X being Element of M holds X = (id M) .. X