theorem :: PZFMISC1:60

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