theorem :: PZFMISC1:58

for I being set
for X, Y being ManySortedSet of I st X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] holds
X = Y