theorem :: MSUALG_9:6

for I being set
for A being ManySortedSet of I ex B being non-empty ManySortedSet of I st A c= B