theorem :: PZFMISC1:58

for I being set
for X, Y being ManySortedSet of I st X is V2() & Y is V2() & [|X,Y|] = [|Y,X|] holds
X = Y