theorem :: PZFMISC1:39

for I being set
for x, X being ManySortedSet of I st x in X holds
{x} (\/) X = X