theorem Th5: :: MSUALG_9:5

for a, I being set ex A being ManySortedSet of I st {A} = I --> {a}