theorem :: PZFMISC1:59

for I being set
for X, Y being ManySortedSet of I st [|X,X|] = [|Y,Y|] holds
X = Y