theorem Th9: :: CLOSURE1:9

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