theorem :: PZFMISC1:35

for I being set
for x1, x2, A being ManySortedSet of I st ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) holds
A c= {x1,x2}