theorem :: PZFMISC1:76

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