theorem Th21: :: MSAFREE4:21

for I being set
for A being ManySortedSet of I
for B being non-empty ManySortedSet of I holds A is_transformable_to B