theorem :: PZFMISC1:77

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