theorem :: PZFMISC1:18

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