theorem :: PZFMISC1:79

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